YES 69.257
↳ HASKELL
↳ LR
((plusFM :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
\oldnew→new
addToFM0 old new = new
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
((plusFM :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord a => FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
case fm_l of EmptyFM → True Branch left_key _ _ _ _ →
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
left_ok0 fm_l key EmptyFM = True left_ok0 fm_l key (Branch left_key _ _ _ _) =
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
case fm_r of EmptyFM → True Branch right_key _ _ _ _ →
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
right_ok0 fm_r key EmptyFM = True right_ok0 fm_r key (Branch right_key _ _ _ _) =
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
case fm_R of Branch _ _ _ fm_rl fm_rr
| sizeFM fm_rl < 2 * sizeFM fm_rr
→ single_L fm_L fm_R | otherwise
→ double_L fm_L fm_R
mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
case fm_L of Branch _ _ _ fm_ll fm_lr
| sizeFM fm_lr < 2 * sizeFM fm_ll
→ single_R fm_L fm_R | otherwise
→ double_R fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
((plusFM :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
fm_l@(Branch yy yz zu zv zw)
Branch yy yz zu zv zw
fm_r@(Branch zy zz vuu vuv vuw)
Branch zy zz vuu vuv vuw
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((plusFM :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap b a -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
splitLT EmptyFM split_key = emptyFM splitLT (Branch key elt xw fm_l fm_r) split_key
| split_key < key
= splitLT fm_l split_key | split_key > key
= mkVBalBranch key elt fm_l (splitLT fm_r split_key) | otherwise
= fm_l
splitLT EmptyFM split_key = splitLT4 EmptyFM split_key splitLT (Branch key elt xw fm_l fm_r) split_key = splitLT3 (Branch key elt xw fm_l fm_r) split_key
splitLT0 key elt xw fm_l fm_r split_key True = fm_l
splitLT1 key elt xw fm_l fm_r split_key True = mkVBalBranch key elt fm_l (splitLT fm_r split_key) splitLT1 key elt xw fm_l fm_r split_key False = splitLT0 key elt xw fm_l fm_r split_key otherwise
splitLT2 key elt xw fm_l fm_r split_key True = splitLT fm_l split_key splitLT2 key elt xw fm_l fm_r split_key False = splitLT1 key elt xw fm_l fm_r split_key (split_key > key)
splitLT3 (Branch key elt xw fm_l fm_r) split_key = splitLT2 key elt xw fm_l fm_r split_key (split_key < key)
splitLT4 EmptyFM split_key = emptyFM splitLT4 vyu vyv = splitLT3 vyu vyv
splitGT EmptyFM split_key = emptyFM splitGT (Branch key elt xx fm_l fm_r) split_key
| split_key > key
= splitGT fm_r split_key | split_key < key
= mkVBalBranch key elt (splitGT fm_l split_key) fm_r | otherwise
= fm_r
splitGT EmptyFM split_key = splitGT4 EmptyFM split_key splitGT (Branch key elt xx fm_l fm_r) split_key = splitGT3 (Branch key elt xx fm_l fm_r) split_key
splitGT1 key elt xx fm_l fm_r split_key True = mkVBalBranch key elt (splitGT fm_l split_key) fm_r splitGT1 key elt xx fm_l fm_r split_key False = splitGT0 key elt xx fm_l fm_r split_key otherwise
splitGT2 key elt xx fm_l fm_r split_key True = splitGT fm_r split_key splitGT2 key elt xx fm_l fm_r split_key False = splitGT1 key elt xx fm_l fm_r split_key (split_key < key)
splitGT0 key elt xx fm_l fm_r split_key True = fm_r
splitGT3 (Branch key elt xx fm_l fm_r) split_key = splitGT2 key elt xx fm_l fm_r split_key (split_key > key)
splitGT4 EmptyFM split_key = emptyFM splitGT4 vyy vyz = splitGT3 vyy vyz
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt mkVBalBranch key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
| sIZE_RATIO * size_l < size_r
= mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw | sIZE_RATIO * size_r < size_l
= mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) | otherwise
= mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw) where
size_l = sizeFM (Branch yy yz zu zv zw)
size_r = sizeFM (Branch zy zz vuu vuv vuw)
mkVBalBranch key elt EmptyFM fm_r = mkVBalBranch5 key elt EmptyFM fm_r mkVBalBranch key elt fm_l EmptyFM = mkVBalBranch4 key elt fm_l EmptyFM mkVBalBranch key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw) = mkVBalBranch3 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch3 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw) =
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_l < size_r) where
mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw otherwise
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch yy yz zu zv zw)
size_r = sizeFM (Branch zy zz vuu vuv vuw)
mkVBalBranch4 key elt fm_l EmptyFM = addToFM fm_l key elt mkVBalBranch4 vzx vzy vzz wuu = mkVBalBranch3 vzx vzy vzz wuu
mkVBalBranch5 key elt EmptyFM fm_r = addToFM fm_r key elt mkVBalBranch5 wuw wux wuy wuz = mkVBalBranch4 wuw wux wuy wuz
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch key elt fm_L fm_R
| size_l + size_r < 2
= mkBranch 1 key elt fm_L fm_R | size_r > sIZE_RATIO * size_l
= mkBalBranch0 fm_L fm_R fm_R | size_l > sIZE_RATIO * size_r
= mkBalBranch1 fm_L fm_R fm_L | otherwise
= mkBranch 2 key elt fm_L fm_R where
double_L fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R
mkBalBranch6 key elt fm_L fm_R =
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where
double_L fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
addToFM_C combiner EmptyFM key elt = unitFM key elt addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt
| new_key < key
= mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r | new_key > key
= mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt) | otherwise
= Branch new_key (combiner elt new_elt) size fm_l fm_r
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt) addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)
addToFM_C4 combiner EmptyFM key elt = unitFM key elt addToFM_C4 wvy wvz wwu wwv = addToFM_C3 wvy wvz wwu wwv
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
((plusFM :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where
double_L fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
mkBalBranch6MkBalBranch00 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr True = mkBalBranch6Double_L www wwx wwy wwz fm_L fm_R
mkBalBranch6Single_L www wwx wwy wwz fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 www wwx fm_l fm_rl) fm_rr
mkBalBranch6MkBalBranch2 www wwx wwy wwz key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch6MkBalBranch01 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr True = mkBalBranch6Single_L www wwx wwy wwz fm_L fm_R mkBalBranch6MkBalBranch01 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch6MkBalBranch00 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch6MkBalBranch11 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr True = mkBalBranch6Single_R www wwx wwy wwz fm_L fm_R mkBalBranch6MkBalBranch11 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch6MkBalBranch10 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch6MkBalBranch4 www wwx wwy wwz key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 www wwx wwy wwz fm_L fm_R fm_R mkBalBranch6MkBalBranch4 www wwx wwy wwz key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 www wwx wwy wwz key elt fm_L fm_R (mkBalBranch6Size_l www wwx wwy wwz > sIZE_RATIO * mkBalBranch6Size_r www wwx wwy wwz)
mkBalBranch6Size_l www wwx wwy wwz = sizeFM wwy
mkBalBranch6MkBalBranch3 www wwx wwy wwz key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 www wwx wwy wwz fm_L fm_R fm_L mkBalBranch6MkBalBranch3 www wwx wwy wwz key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 www wwx wwy wwz key elt fm_L fm_R otherwise
mkBalBranch6MkBalBranch02 www wwx wwy wwz fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch6MkBalBranch01 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch6MkBalBranch12 www wwx wwy wwz fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch6MkBalBranch11 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch6Double_R www wwx wwy wwz (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 www wwx fm_lrr fm_r)
mkBalBranch6MkBalBranch1 www wwx wwy wwz fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch6MkBalBranch12 www wwx wwy wwz fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch6Double_L www wwx wwy wwz fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 www wwx fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
mkBalBranch6MkBalBranch0 www wwx wwy wwz fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch6MkBalBranch02 www wwx wwy wwz fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
mkBalBranch6MkBalBranch10 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr True = mkBalBranch6Double_R www wwx wwy wwz fm_L fm_R
mkBalBranch6Single_R www wwx wwy wwz (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 www wwx fm_lr fm_r)
mkBalBranch6MkBalBranch5 www wwx wwy wwz key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch6MkBalBranch5 www wwx wwy wwz key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 www wwx wwy wwz key elt fm_L fm_R (mkBalBranch6Size_r www wwx wwy wwz > sIZE_RATIO * mkBalBranch6Size_l www wwx wwy wwz)
mkBalBranch6Size_r www wwx wwy wwz = sizeFM wwz
let
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r in result where
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True left_ok0 fm_l key (Branch left_key wu wv ww wx) =
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True right_ok0 fm_r key (Branch right_key vw vx vy vz) =
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
right_size = sizeFM fm_r
unbox x = x
mkBranchBalance_ok wxu wxv wxw = True
mkBranchUnbox wxu wxv wxw x = x
mkBranchLeft_ok0 wxu wxv wxw fm_l key EmptyFM = True mkBranchLeft_ok0 wxu wxv wxw fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key
mkBranchRight_ok wxu wxv wxw = mkBranchRight_ok0 wxu wxv wxw wxu wxv wxu
mkBranchLeft_size wxu wxv wxw = sizeFM wxw
mkBranchRight_ok0 wxu wxv wxw fm_r key EmptyFM = True mkBranchRight_ok0 wxu wxv wxw fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r
mkBranchLeft_ok wxu wxv wxw = mkBranchLeft_ok0 wxu wxv wxw wxw wxv wxw
mkBranchRight_size wxu wxv wxw = sizeFM wxu
let
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r in result
mkBranchResult wxx wxy wxz wyu = Branch wxx wxy (mkBranchUnbox wxz wxx wyu (1 + mkBranchLeft_size wxz wxx wyu + mkBranchRight_size wxz wxx wyu)) wyu wxz
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_l < size_r) where
mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw otherwise
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch yy yz zu zv zw)
size_r = sizeFM (Branch zy zz vuu vuv vuw)
mkVBalBranch3Size_l wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy = sizeFM (Branch wyv wyw wyx wyy wyz)
mkVBalBranch3MkVBalBranch0 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch3MkVBalBranch1 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) mkVBalBranch3MkVBalBranch1 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch3MkVBalBranch0 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw otherwise
mkVBalBranch3Size_r wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy = sizeFM (Branch wzu wzv wzw wzx wzy)
mkVBalBranch3MkVBalBranch2 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw mkVBalBranch3MkVBalBranch2 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch3MkVBalBranch1 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * mkVBalBranch3Size_r wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy < mkVBalBranch3Size_l wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy)
mkVBalBranch split_key elt1 (plusFM lts left) (plusFM gts right) where
gts = splitGT fm1 split_key
lts = splitLT fm1 split_key
plusFMGts wzz xuu = splitGT wzz xuu
plusFMLts wzz xuu = splitLT wzz xuu
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
mkBranchLeft_ok0Biggest_left_key xuv = fst (findMax xuv)
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
mkBranchRight_ok0Smallest_right_key xuw = fst (findMin xuw)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
((plusFM :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) |
import qualified Maybe import qualified Prelude |
|||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> a ( -> (FiniteMap a b) (Int -> Int)))
|
|||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||
sizeFM :: FiniteMap b a -> Int
|
|||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
(plusFM :: FiniteMap Int a -> FiniteMap Int a -> FiniteMap Int a) |
import qualified Maybe import qualified Prelude |
|||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> a ( -> (FiniteMap a b) (Int -> Int)))
|
|||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
plusFM :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_esEs(Succ(xux1977000), Succ(xux1972000)) → new_esEs(xux1977000, xux1972000)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_esEs0(Succ(xux5200000000), Succ(xux18190)) → new_esEs0(xux5200000000, xux18190)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_primMinusNat(Succ(xux129700), Succ(xux12430)) → new_primMinusNat(xux129700, xux12430)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_primPlusNat(Succ(xux1020000), Succ(xux542000)) → new_primPlusNat(xux1020000, xux542000)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_mkBalBranch6MkBalBranch4(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux1956000), Succ(xux1955000), h, ba) → new_mkBalBranch6MkBalBranch4(xux5260, xux5261, xux1959, xux5264, xux1958, xux1956000, xux1955000, h, ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_addToFM_C3(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, bd, be) → new_addToFM_C2(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, new_lt0(xux528, xux5220, bd), bd, be)
new_addToFM_C2(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, True, bb, bc) → new_addToFM_C0(xux1975, xux1977, xux1978, bb, bc)
new_addToFM_C2(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, False, bb, bc) → new_addToFM_C1(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, new_gt(xux1977, xux1972, bb), bb, bc)
new_addToFM_C2(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, True, bb, bc) → new_mkBalBranch6MkBalBranch50(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, new_lt(new_ps(new_mkBalBranch6Size_l(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc), new_mkBalBranch6Size_r(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc)), Pos(Succ(Succ(Zero)))), bb, bc)
new_addToFM_C1(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, True, h, ba) → new_addToFM_C0(xux1993, xux1994, xux1995, h, ba)
new_mkBalBranch6MkBalBranch5(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, False, h, ba) → new_addToFM_C0(xux1993, xux1994, xux1995, h, ba)
new_addToFM_C0(Branch(xux19750, xux19751, xux19752, xux19753, xux19754), xux1977, xux1978, bb, bc) → new_addToFM_C3(xux19750, xux19751, xux19752, xux19753, xux19754, xux1977, xux1978, bb, bc)
new_addToFM_C2(xux1972, xux1973, xux1974, Branch(xux19750, xux19751, xux19752, xux19753, xux19754), xux1976, xux1977, xux1978, True, bb, bc) → new_addToFM_C3(xux19750, xux19751, xux19752, xux19753, xux19754, xux1977, xux1978, bb, bc)
new_mkBalBranch6MkBalBranch50(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, False, bb, bc) → new_addToFM_C0(xux1975, xux1977, xux1978, bb, bc)
new_addToFM_C1(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, True, h, ba) → new_mkBalBranch6MkBalBranch5(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, new_lt(new_ps(new_mkBalBranch6Size_l(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), h, ba), new_mkBalBranch6Size_r(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), h, ba)), Pos(Succ(Succ(Zero)))), h, ba)
new_mkBalBranch6MkBalBranch5(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, True, h, ba) → new_addToFM_C0(xux1993, xux1994, xux1995, h, ba)
new_mkBalBranch6MkBalBranch50(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, True, bb, bc) → new_addToFM_C0(xux1975, xux1977, xux1978, bb, bc)
new_esEs10(Pos(Zero), Pos(Zero)) → new_esEs1
new_primMulNat(xux500) → new_primPlusNat0(new_primPlusNat0(new_primMulNat0(xux500), Succ(xux500)), Succ(xux500))
new_lt0(xux528, xux5220, ty_Integer) → error([])
new_gt0(Neg(Zero), Neg(Zero)) → new_esEs9
new_gt(xux1977, xux1972, ty_Integer) → error([])
new_esEs5 → False
new_gt0(Pos(Zero), Pos(Zero)) → new_esEs9
new_lt0(xux528, xux5220, ty_Char) → error([])
new_lt0(xux528, xux5220, app(ty_Ratio, ed)) → error([])
new_mkBalBranch6Size_l(xux5260, xux5261, xux1866, xux5264, bd, be) → new_sizeFM(xux1866, bd, be)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Pos(Zero), bd, be) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Neg(Zero), bd, be) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_addToFM_C(EmptyFM, xux1977, xux1978, bb, bc) → Branch(xux1977, xux1978, Pos(Succ(Zero)), new_emptyFM(bb, bc), new_emptyFM(bb, bc))
new_addToFM_C(Branch(xux19750, xux19751, xux19752, xux19753, xux19754), xux1977, xux1978, bb, bc) → new_addToFM_C30(xux19750, xux19751, xux19752, xux19753, xux19754, xux1977, xux1978, bb, bc)
new_gt(xux1977, xux1972, ty_Float) → error([])
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Neg(Succ(xux195500)), bd, be) → new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195500, Zero, bd, be)
new_ps(Neg(xux19360), Neg(xux19350)) → Neg(new_primPlusNat0(xux19360, xux19350))
new_esEs2(Zero, Succ(xux18190)) → new_esEs4
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, Branch(xux195840, xux195841, xux195842, xux195843, xux195844), False, bd, be) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))), xux195840, xux195841, new_mkBranch0(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))), xux19580, xux19581, xux19583, xux195843, bd, be), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))), xux5260, xux5261, xux195844, xux5264, bd, be)
new_esEs2(Succ(xux5200000000), Zero) → new_esEs3
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Neg(Succ(xux195500)), bd, be) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be) → new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, xux1958, new_gt0(new_mkBalBranch6Size_l(xux5260, xux5261, xux1959, xux5264, bd, be), new_sr0(new_mkBalBranch6Size_r(xux5260, xux5261, xux1959, xux5264, bd, be))), bd, be)
new_gt(xux1977, xux1972, app(app(app(ty_@3, cd), ce), cf)) → error([])
new_esEs10(Neg(Succ(xux52800)), Neg(xux5190)) → new_esEs2(xux5190, Succ(xux52800))
new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, True, bb, bc) → new_mkBranch1(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc)
new_gt(xux1977, xux1972, ty_Char) → error([])
new_addToFM_C20(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, False, bb, bc) → new_addToFM_C10(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, new_gt(xux1977, xux1972, bb), bb, bc)
new_esEs10(Pos(Succ(xux52800)), Neg(xux5190)) → new_esEs3
new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, Branch(xux52640, xux52641, xux52642, xux52643, xux52644), xux1958, bd, be) → new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, xux52643, xux52644, xux1958, new_lt(new_sizeFM(xux52643, bd, be), new_sr(new_sizeFM(xux52644, bd, be))), bd, be)
new_mkBranchUnbox(xux5264, xux5260, xux1960, xux1961, bd, be) → xux1961
new_gt(xux1977, xux1972, ty_@0) → error([])
new_gt(xux1977, xux1972, ty_Ordering) → error([])
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux1956000), Succ(xux1955000), bd, be) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux1956000, xux1955000, bd, be)
new_gt(xux1977, xux1972, app(ty_Ratio, cg)) → error([])
new_primMulInt0(Neg(xux18400)) → Neg(new_primMulNat3(xux18400))
new_emptyFM(bb, bc) → EmptyFM
new_gt0(Pos(Succ(xux197700)), Neg(xux19720)) → new_esEs8
new_gt0(Neg(Zero), Neg(Succ(xux197200))) → new_esEs6(xux197200, Zero)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Neg(Zero), bd, be) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_primMulInt0(Pos(xux18400)) → Pos(new_primMulNat3(xux18400))
new_lt0(xux528, xux5220, app(ty_[], dd)) → error([])
new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, Zero, bd, be) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_addToFM_C30(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, bd, be) → new_addToFM_C20(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, new_lt0(xux528, xux5220, bd), bd, be)
new_lt(xux528, xux519) → new_esEs10(xux528, xux519)
new_lt0(xux528, xux5220, app(app(app(ty_@3, ea), eb), ec)) → error([])
new_primMulNat3(Zero) → Zero
new_esEs10(Pos(Succ(xux52800)), Pos(xux5190)) → new_esEs2(Succ(xux52800), xux5190)
new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be) → new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, xux19584, True, bd, be) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))), xux19580, xux19581, xux19583, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))), xux5260, xux5261, xux19584, xux5264, bd, be)
new_sr0(xux1919) → new_primMulInt(xux1919)
new_primMulNat0(xux500) → new_primPlusNat0(Zero, Succ(xux500))
new_gt0(Pos(Zero), Pos(Succ(xux197200))) → new_esEs11(Zero, xux197200)
new_primMinusNat0(Zero, Succ(xux12430)) → Neg(Succ(xux12430))
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, Zero, bd, be) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_esEs7(Succ(xux1977000), Succ(xux1972000)) → new_esEs7(xux1977000, xux1972000)
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, xux52643, xux52644, xux1958, True, bd, be) → new_mkBranchResult(xux52640, xux52641, xux52644, new_mkBranchResult(xux5260, xux5261, xux52643, xux1958, bd, be), bd, be)
new_lt0(xux528, xux5220, app(app(ty_@2, de), df)) → error([])
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Succ(xux195600)), Pos(xux19550), bd, be) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_ps(Pos(xux19360), Pos(xux19350)) → Pos(new_primPlusNat0(xux19360, xux19350))
new_esEs9 → False
new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be) → new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_esEs8 → True
new_gt0(Neg(Zero), Pos(Succ(xux197200))) → new_esEs5
new_ps(Pos(xux19360), Neg(xux19350)) → new_primMinusNat0(xux19360, xux19350)
new_ps(Neg(xux19360), Pos(xux19350)) → new_primMinusNat0(xux19350, xux19360)
new_lt0(xux528, xux5220, ty_Bool) → error([])
new_gt(xux1977, xux1972, ty_Int) → new_gt0(xux1977, xux1972)
new_mkBalBranch6Size_r(xux5260, xux5261, xux1875, xux5264, bd, be) → new_sizeFM(xux5264, bd, be)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Succ(xux195600)), Neg(xux19550), bd, be) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_esEs10(Neg(Zero), Pos(Zero)) → new_esEs1
new_esEs10(Pos(Zero), Neg(Zero)) → new_esEs1
new_gt0(Pos(Succ(xux197700)), Pos(xux19720)) → new_esEs6(xux197700, xux19720)
new_esEs10(Neg(Succ(xux52800)), Pos(xux5190)) → new_esEs4
new_sr(Neg(xux20120)) → Neg(new_primMulNat2(xux20120))
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Succ(xux195600)), Pos(xux19550), bd, be) → new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, xux19550, bd, be)
new_primMulNat1(xux500) → new_primPlusNat0(new_primMulNat(xux500), Succ(xux500))
new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, False, h, ba) → new_mkBalBranch6MkBalBranch40(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), xux1992, new_mkBalBranch6Size_r(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), h, ba), new_sr0(new_mkBalBranch6Size_l(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), h, ba)), h, ba)
new_addToFM_C20(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, True, bb, bc) → new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, new_lt(new_ps(new_mkBalBranch6Size_l(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc), new_mkBalBranch6Size_r(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc)), Pos(Succ(Succ(Zero)))), bb, bc)
new_mkBranch(xux2028, xux2029, xux2030, xux2031, xux2032, xux2033, xux2034, xux2035, xux2036, ee, ef) → new_mkBranchResult(xux2029, xux2030, new_mkBranch0(xux2032, xux2033, xux2034, xux2035, xux2036, ee, ef), xux2031, ee, ef)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Pos(Succ(xux195500)), bd, be) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_primMulInt(xux1859) → new_primMulInt0(xux1859)
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, xux1958, False, bd, be) → new_mkBranchResult(xux5260, xux5261, xux5264, xux1958, bd, be)
new_esEs10(Pos(Zero), Neg(Succ(xux51900))) → new_esEs3
new_gt0(Pos(Zero), Neg(Succ(xux197200))) → new_esEs8
new_lt0(xux528, xux5220, ty_@0) → error([])
new_gt(xux1977, xux1972, app(ty_Maybe, bf)) → error([])
new_esEs10(Neg(Zero), Neg(Zero)) → new_esEs1
new_primPlusNat0(Succ(xux1020000), Succ(xux542000)) → Succ(Succ(new_primPlusNat0(xux1020000, xux542000)))
new_esEs7(Zero, Zero) → new_esEs9
new_esEs7(Zero, Succ(xux1972000)) → new_esEs5
new_esEs4 → True
new_lt0(xux528, xux5220, ty_Int) → new_lt(xux528, xux5220)
new_esEs11(Zero, xux197700) → new_esEs5
new_primPlusNat0(Zero, Zero) → Zero
new_gt(xux1977, xux1972, ty_Double) → error([])
new_esEs6(xux197700, Zero) → new_esEs8
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, Succ(xux1955000), bd, be) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_esEs6(xux197700, Succ(xux197200)) → new_esEs7(xux197700, xux197200)
new_primMinusNat0(Succ(xux129700), Zero) → Pos(Succ(xux129700))
new_primMulNat3(Succ(xux184000)) → new_primPlusNat0(new_primMulNat1(xux184000), Succ(xux184000))
new_sizeFM(EmptyFM, da, db) → Pos(Zero)
new_gt(xux1977, xux1972, app(ty_[], bg)) → error([])
new_mkBranch1(xux1989, xux1990, xux1992, xux2013, h, ba) → new_mkBranchResult(xux1989, xux1990, xux2013, xux1992, h, ba)
new_esEs10(Pos(Zero), Pos(Succ(xux51900))) → new_esEs2(Zero, Succ(xux51900))
new_esEs2(Zero, Zero) → new_esEs1
new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, Succ(xux195500), bd, be) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, xux195500, bd, be)
new_sizeFM(Branch(xux15350, xux15351, xux15352, xux15353, xux15354), da, db) → xux15352
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, EmptyFM, xux52644, xux1958, False, bd, be) → error([])
new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, EmptyFM, xux1958, bd, be) → error([])
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, EmptyFM, True, bd, be) → error([])
new_esEs11(Succ(xux197200), xux197700) → new_esEs7(xux197200, xux197700)
new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, False, bb, bc) → new_mkBalBranch6MkBalBranch40(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), new_mkBalBranch6Size_r(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc), new_sr0(new_mkBalBranch6Size_l(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc)), bb, bc)
new_lt0(xux528, xux5220, app(ty_Maybe, dc)) → error([])
new_gt(xux1977, xux1972, ty_Bool) → error([])
new_esEs10(Neg(Zero), Pos(Succ(xux51900))) → new_esEs4
new_esEs1 → False
new_lt0(xux528, xux5220, ty_Double) → error([])
new_esEs3 → False
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_esEs7(Succ(xux1977000), Zero) → new_esEs8
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, Branch(xux526430, xux526431, xux526432, xux526433, xux526434), xux52644, xux1958, False, bd, be) → new_mkBranch(Succ(Succ(Succ(Succ(Zero)))), xux526430, xux526431, new_mkBranchResult(xux5260, xux5261, xux526433, xux1958, bd, be), Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))), xux52640, xux52641, xux526434, xux52644, bd, be)
new_addToFM_C10(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, False, h, ba) → Branch(xux1994, xux1995, xux1991, xux1992, xux1993)
new_addToFM_C10(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, True, h, ba) → new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, new_lt(new_ps(new_mkBalBranch6Size_l(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), h, ba), new_mkBalBranch6Size_r(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), h, ba)), Pos(Succ(Succ(Zero)))), h, ba)
new_gt0(Neg(Succ(xux197700)), Pos(xux19720)) → new_esEs5
new_primMulNat2(Zero) → Zero
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux1956000), Zero, bd, be) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_lt0(xux528, xux5220, app(app(ty_Either, dg), dh)) → error([])
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Succ(xux195600)), Neg(xux19550), bd, be) → new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, xux19550, xux195600, bd, be)
new_mkBranchResult(xux5260, xux5261, xux5264, xux1960, bd, be) → Branch(xux5260, xux5261, new_mkBranchUnbox(xux5264, xux5260, xux1960, new_ps(new_ps(Pos(Succ(Zero)), new_sizeFM(xux1960, bd, be)), new_sizeFM(xux5264, bd, be)), bd, be), xux1960, xux5264)
new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, xux195600, bd, be) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, EmptyFM, False, bd, be) → error([])
new_lt0(xux528, xux5220, ty_Float) → error([])
new_gt(xux1977, xux1972, app(app(ty_@2, bh), ca)) → error([])
new_esEs2(Succ(xux5200000000), Succ(xux18190)) → new_esEs2(xux5200000000, xux18190)
new_gt0(Neg(Succ(xux197700)), Neg(xux19720)) → new_esEs11(xux19720, xux197700)
new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, True, h, ba) → new_mkBranch1(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, h, ba), h, ba)
new_lt0(xux528, xux5220, ty_Ordering) → error([])
new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux195500), xux195600, bd, be) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux195500, xux195600, bd, be)
new_esEs10(Neg(Zero), Neg(Succ(xux51900))) → new_esEs2(Succ(xux51900), Zero)
new_primMulNat2(Succ(xux201200)) → new_primPlusNat0(new_primMulNat0(xux201200), Succ(xux201200))
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Pos(Zero), bd, be) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, bd, be)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Pos(Succ(xux195500)), bd, be) → new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, xux195500, bd, be)
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, Branch(xux19580, xux19581, xux19582, xux19583, xux19584), True, bd, be) → new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, xux19584, new_lt(new_sizeFM(xux19584, bd, be), new_sr(new_sizeFM(xux19583, bd, be))), bd, be)
new_sr(Pos(xux20120)) → Pos(new_primMulNat2(xux20120))
new_primPlusNat0(Succ(xux1020000), Zero) → Succ(xux1020000)
new_primPlusNat0(Zero, Succ(xux542000)) → Succ(xux542000)
new_gt0(Pos(Zero), Neg(Zero)) → new_esEs9
new_gt0(Neg(Zero), Pos(Zero)) → new_esEs9
new_mkBranch0(xux2032, xux2033, xux2034, xux2035, xux2036, ee, ef) → new_mkBranchResult(xux2033, xux2034, xux2036, xux2035, ee, ef)
new_gt(xux1977, xux1972, app(app(ty_Either, cb), cc)) → error([])
new_primMinusNat0(Succ(xux129700), Succ(xux12430)) → new_primMinusNat0(xux129700, xux12430)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, EmptyFM, x6, x7, False, x8, x9)
new_ps(Neg(x0), Neg(x1))
new_gt(x0, x1, ty_@0)
new_gt0(Pos(Zero), Pos(Succ(x0)))
new_lt0(x0, x1, ty_Float)
new_addToFM_C(EmptyFM, x0, x1, x2, x3)
new_gt(x0, x1, app(app(ty_@2, x2), x3))
new_gt0(Neg(Zero), Pos(Succ(x0)))
new_gt0(Pos(Zero), Neg(Succ(x0)))
new_gt(x0, x1, ty_Char)
new_gt(x0, x1, ty_Ordering)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Pos(Zero), x5, x6)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Neg(Zero), x5, x6)
new_gt0(Pos(Succ(x0)), Pos(x1))
new_primMinusNat0(Zero, Zero)
new_mkBranch0(x0, x1, x2, x3, x4, x5, x6)
new_esEs5
new_addToFM_C30(x0, x1, x2, x3, x4, x5, x6, x7, x8)
new_emptyFM(x0, x1)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Succ(x5)), Neg(x6), x7, x8)
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_primMulNat3(Succ(x0))
new_esEs7(Zero, Zero)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_esEs10(Neg(Zero), Neg(Succ(x0)))
new_mkBalBranch6MkBalBranch41(x0, x1, x2, x3, x4, x5, Succ(x6), x7, x8)
new_sizeFM(EmptyFM, x0, x1)
new_esEs7(Succ(x0), Succ(x1))
new_lt0(x0, x1, ty_@0)
new_gt(x0, x1, ty_Bool)
new_lt0(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat(x0)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Pos(Zero), x5, x6)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Neg(Succ(x5)), x6, x7)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Pos(Succ(x5)), x6, x7)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Neg(Succ(x5)), x6, x7)
new_mkBalBranch6MkBalBranch47(x0, x1, x2, x3, x4, x5, x6)
new_ps(Neg(x0), Pos(x1))
new_ps(Pos(x0), Neg(x1))
new_gt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_gt(x0, x1, app(ty_Maybe, x2))
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, x4, False, x5, x6)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Zero, Succ(x5), x6, x7)
new_primMulInt0(Neg(x0))
new_primMulNat2(Succ(x0))
new_gt(x0, x1, ty_Integer)
new_lt0(x0, x1, ty_Ordering)
new_mkBalBranch6MkBalBranch45(x0, x1, x2, x3, x4, x5, x6)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_gt(x0, x1, ty_Double)
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_lt0(x0, x1, ty_Char)
new_lt0(x0, x1, app(ty_Ratio, x2))
new_lt0(x0, x1, ty_Bool)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs8
new_mkBalBranch6MkBalBranch43(x0, x1, x2, x3, x4, Succ(x5), x6, x7, x8)
new_esEs6(x0, Succ(x1))
new_mkBalBranch6MkBalBranch42(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, x9, x10)
new_esEs9
new_primMinusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Succ(x0))
new_esEs10(Pos(Zero), Neg(Zero))
new_esEs10(Neg(Zero), Pos(Zero))
new_mkBalBranch6MkBalBranch52(x0, x1, x2, x3, x4, x5, True, x6, x7)
new_primMulNat0(x0)
new_mkBranchResult(x0, x1, x2, x3, x4, x5)
new_lt0(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(Pos(Succ(x0)), Neg(x1))
new_esEs10(Neg(Succ(x0)), Pos(x1))
new_mkBalBranch6MkBalBranch42(x0, x1, x2, EmptyFM, x3, x4, x5)
new_esEs3
new_gt0(Neg(Succ(x0)), Pos(x1))
new_gt0(Pos(Succ(x0)), Neg(x1))
new_esEs7(Zero, Succ(x0))
new_sr0(x0)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Succ(x5)), Pos(x6), x7, x8)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Succ(x5)), Neg(x6), x7, x8)
new_mkBranch(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
new_gt0(Pos(Zero), Neg(Zero))
new_gt0(Neg(Zero), Pos(Zero))
new_primMulInt(x0)
new_esEs4
new_primPlusNat0(Succ(x0), Zero)
new_esEs7(Succ(x0), Zero)
new_esEs10(Neg(Succ(x0)), Neg(x1))
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Succ(x5)), Pos(x6), x7, x8)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Neg(Zero), x5, x6)
new_lt(x0, x1)
new_lt0(x0, x1, app(ty_[], x2))
new_esEs10(Pos(Zero), Pos(Succ(x0)))
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Zero, Zero, x5, x6)
new_mkBalBranch6Size_l(x0, x1, x2, x3, x4, x5)
new_mkBalBranch6MkBalBranch43(x0, x1, x2, x3, x4, Zero, x5, x6, x7)
new_ps(Pos(x0), Pos(x1))
new_lt0(x0, x1, ty_Double)
new_primPlusNat0(Zero, Zero)
new_esEs11(Zero, x0)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, EmptyFM, False, x8, x9)
new_mkBranchUnbox(x0, x1, x2, x3, x4, x5)
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_primMulInt0(Pos(x0))
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, Branch(x4, x5, x6, x7, x8), True, x9, x10)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, Branch(x6, x7, x8, x9, x10), x11, x12, False, x13, x14)
new_esEs10(Neg(Zero), Neg(Zero))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_gt(x0, x1, app(ty_Ratio, x2))
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Succ(x5), Succ(x6), x7, x8)
new_esEs6(x0, Zero)
new_gt0(Neg(Zero), Neg(Zero))
new_esEs2(Zero, Succ(x0))
new_primMinusNat0(Succ(x0), Zero)
new_esEs11(Succ(x0), x1)
new_mkBalBranch6MkBalBranch52(x0, x1, x2, x3, x4, x5, False, x6, x7)
new_esEs10(Neg(Zero), Pos(Succ(x0)))
new_esEs10(Pos(Succ(x0)), Pos(x1))
new_esEs10(Pos(Zero), Neg(Succ(x0)))
new_primMulNat2(Zero)
new_mkBalBranch6MkBalBranch41(x0, x1, x2, x3, x4, x5, Zero, x6, x7)
new_addToFM_C(Branch(x0, x1, x2, x3, x4), x5, x6, x7, x8)
new_esEs2(Succ(x0), Zero)
new_sr(Pos(x0))
new_gt0(Neg(Zero), Neg(Succ(x0)))
new_lt0(x0, x1, ty_Int)
new_lt0(x0, x1, app(app(ty_@2, x2), x3))
new_gt0(Pos(Zero), Pos(Zero))
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Succ(x5), Zero, x6, x7)
new_mkBalBranch6MkBalBranch51(x0, x1, x2, x3, x4, x5, True, x6, x7)
new_esEs2(Succ(x0), Succ(x1))
new_primMulNat1(x0)
new_esEs10(Pos(Zero), Pos(Zero))
new_sr(Neg(x0))
new_esEs1
new_primMinusNat0(Succ(x0), Succ(x1))
new_mkBranch1(x0, x1, x2, x3, x4, x5)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, Branch(x8, x9, x10, x11, x12), False, x13, x14)
new_lt0(x0, x1, ty_Integer)
new_gt(x0, x1, ty_Int)
new_gt(x0, x1, app(ty_[], x2))
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, EmptyFM, True, x4, x5)
new_mkBalBranch6Size_r(x0, x1, x2, x3, x4, x5)
new_gt(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat3(Zero)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Pos(Succ(x5)), x6, x7)
new_gt0(Neg(Succ(x0)), Neg(x1))
new_mkBalBranch6MkBalBranch51(x0, x1, x2, x3, x4, x5, False, x6, x7)
new_lt0(x0, x1, app(ty_Maybe, x2))
new_esEs2(Zero, Zero)
new_gt(x0, x1, ty_Float)
new_mkBalBranch6MkBalBranch44(x0, x1, x2, x3, x4, x5, x6)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_mkVBalBranch3MkVBalBranch1(xux5220, xux5221, xux5222, xux5223, Branch(xux52240, xux52241, xux52242, xux52243, xux52244), xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, h, ba) → new_mkVBalBranch3(xux528, xux529, xux52240, xux52241, xux52242, xux52243, xux52244, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)
new_mkVBalBranch2(xux528, xux529, Branch(xux52240, xux52241, xux52242, xux52243, xux52244), xux5260, xux5261, xux5262, xux5263, xux5264, h, ba) → new_mkVBalBranch3(xux528, xux529, xux52240, xux52241, xux52242, xux52243, xux52244, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)
new_mkBalBranch6MkBalBranch53(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, False, h, ba) → new_mkVBalBranch0(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba)
new_mkBalBranch6MkBalBranch53(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, True, h, ba) → new_mkVBalBranch0(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba)
new_mkBalBranch6MkBalBranch54(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, False, h, ba) → new_mkVBalBranch2(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)
new_mkVBalBranch3MkVBalBranch2(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, Branch(xux52630, xux52631, xux52632, xux52633, xux52634), xux5264, xux528, xux529, True, h, ba) → new_mkVBalBranch3MkVBalBranch2(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, h, ba) → new_mkVBalBranch0(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba)
new_mkVBalBranch3(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba) → new_mkVBalBranch3MkVBalBranch2(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch1(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, h, ba) → new_mkBalBranch6MkBalBranch54(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, new_lt(new_ps(new_mkBalBranch6Size_l(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), h, ba), new_mkBalBranch6Size_r(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), h, ba)), Pos(Succ(Succ(Zero)))), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, False, h, ba) → new_mkVBalBranch3MkVBalBranch1(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)), new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)), h, ba)
new_mkVBalBranch0(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, Branch(xux52630, xux52631, xux52632, xux52633, xux52634), h, ba) → new_mkVBalBranch3MkVBalBranch2(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, h, ba) → new_mkBalBranch6MkBalBranch53(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, new_lt(new_ps(new_mkBalBranch6Size_l(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, h, ba), new_mkBalBranch6Size_r(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, h, ba)), Pos(Succ(Succ(Zero)))), h, ba)
new_mkBalBranch6MkBalBranch54(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, True, h, ba) → new_mkVBalBranch2(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)
new_mkVBalBranch3MkVBalBranch1(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, h, ba) → new_mkVBalBranch2(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)
new_esEs10(Pos(Zero), Pos(Zero)) → new_esEs1
new_mkBalBranch6MkBalBranch56(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, True, h, ba) → new_mkBranch1(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, h, ba)
new_primMulNat(xux500) → new_primPlusNat0(new_primPlusNat0(new_primMulNat0(xux500), Succ(xux500)), Succ(xux500))
new_lt0(xux528, xux5220, ty_Integer) → error([])
new_gt0(Neg(Zero), Neg(Zero)) → new_esEs9
new_gt(xux1977, xux1972, ty_Integer) → error([])
new_esEs5 → False
new_gt0(Pos(Zero), Pos(Zero)) → new_esEs9
new_lt0(xux528, xux5220, ty_Char) → error([])
new_lt0(xux528, xux5220, app(ty_Ratio, eh)) → error([])
new_mkBalBranch6Size_l(xux5260, xux5261, xux1866, xux5264, h, ba) → new_sizeFM(xux1866, h, ba)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Neg(Zero), h, ba) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Pos(Zero), h, ba) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_addToFM_C(EmptyFM, xux1977, xux1978, bb, bc) → Branch(xux1977, xux1978, Pos(Succ(Zero)), new_emptyFM(bb, bc), new_emptyFM(bb, bc))
new_addToFM_C(Branch(xux19750, xux19751, xux19752, xux19753, xux19754), xux1977, xux1978, bb, bc) → new_addToFM_C30(xux19750, xux19751, xux19752, xux19753, xux19754, xux1977, xux1978, bb, bc)
new_mkBalBranch6MkBalBranch56(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, False, h, ba) → new_mkBalBranch6MkBalBranch40(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), new_mkBalBranch6Size_r(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, h, ba), new_sr0(new_mkBalBranch6Size_l(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, h, ba)), h, ba)
new_gt(xux1977, xux1972, ty_Float) → error([])
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Neg(Succ(xux195500)), h, ba) → new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195500, Zero, h, ba)
new_ps(Neg(xux19360), Neg(xux19350)) → Neg(new_primPlusNat0(xux19360, xux19350))
new_esEs2(Zero, Succ(xux18190)) → new_esEs4
new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, Branch(xux52630, xux52631, xux52632, xux52633, xux52634), h, ba) → new_mkVBalBranch30(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, Branch(xux195840, xux195841, xux195842, xux195843, xux195844), False, h, ba) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))), xux195840, xux195841, new_mkBranch0(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))), xux19580, xux19581, xux19583, xux195843, h, ba), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))), xux5260, xux5261, xux195844, xux5264, h, ba)
new_esEs2(Succ(xux5200000000), Zero) → new_esEs3
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Neg(Succ(xux195500)), h, ba) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba) → new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, xux1958, new_gt0(new_mkBalBranch6Size_l(xux5260, xux5261, xux1959, xux5264, h, ba), new_sr0(new_mkBalBranch6Size_r(xux5260, xux5261, xux1959, xux5264, h, ba))), h, ba)
new_gt(xux1977, xux1972, app(app(app(ty_@3, cb), cc), cd)) → error([])
new_esEs10(Neg(Succ(xux52800)), Neg(xux5190)) → new_esEs2(xux5190, Succ(xux52800))
new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba) → new_sizeFM(Branch(xux5260, xux5261, xux5262, xux5263, xux5264), h, ba)
new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, True, bb, bc) → new_mkBranch1(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc)
new_gt(xux1977, xux1972, ty_Char) → error([])
new_addToFM_C20(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, False, bb, bc) → new_addToFM_C10(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, new_gt(xux1977, xux1972, bb), bb, bc)
new_esEs10(Pos(Succ(xux52800)), Neg(xux5190)) → new_esEs3
new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, Branch(xux52640, xux52641, xux52642, xux52643, xux52644), xux1958, h, ba) → new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, xux52643, xux52644, xux1958, new_lt(new_sizeFM(xux52643, h, ba), new_sr(new_sizeFM(xux52644, h, ba))), h, ba)
new_mkBranchUnbox(xux5264, xux5260, xux1960, xux1961, h, ba) → xux1961
new_gt(xux1977, xux1972, ty_@0) → error([])
new_gt(xux1977, xux1972, ty_Ordering) → error([])
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux1956000), Succ(xux1955000), h, ba) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux1956000, xux1955000, h, ba)
new_gt(xux1977, xux1972, app(ty_Ratio, ce)) → error([])
new_primMulInt0(Neg(xux18400)) → Neg(new_primMulNat3(xux18400))
new_emptyFM(bb, bc) → EmptyFM
new_gt0(Pos(Succ(xux197700)), Neg(xux19720)) → new_esEs8
new_gt0(Neg(Zero), Neg(Succ(xux197200))) → new_esEs6(xux197200, Zero)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Neg(Zero), h, ba) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_primMulInt0(Pos(xux18400)) → Pos(new_primMulNat3(xux18400))
new_lt0(xux528, xux5220, app(ty_[], dh)) → error([])
new_mkBranch2(xux1938, xux1939, xux1940, xux1941, xux1942, xux1943, xux1944, xux1945, xux1946, xux1947, xux1948, xux1949, xux1950, da, db) → new_mkBranchResult(xux1939, xux1940, Branch(xux1946, xux1947, xux1948, xux1949, xux1950), Branch(xux1941, xux1942, xux1943, xux1944, xux1945), da, db)
new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, Zero, h, ba) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_mkVBalBranch1(xux528, xux529, EmptyFM, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba) → new_addToFM(xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, h, ba)
new_addToFM_C30(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, h, ba) → new_addToFM_C20(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, new_lt0(xux528, xux5220, h), h, ba)
new_lt(xux528, xux519) → new_esEs10(xux528, xux519)
new_lt0(xux528, xux5220, app(app(app(ty_@3, ee), ef), eg)) → error([])
new_primMulNat3(Zero) → Zero
new_mkVBalBranch3MkVBalBranch20(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, False, h, ba) → new_mkVBalBranch3MkVBalBranch10(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)), new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)), h, ba)
new_esEs10(Pos(Succ(xux52800)), Pos(xux5190)) → new_esEs2(Succ(xux52800), xux5190)
new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba) → new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, xux19584, True, h, ba) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))), xux19580, xux19581, xux19583, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))), xux5260, xux5261, xux19584, xux5264, h, ba)
new_sr0(xux1919) → new_primMulInt(xux1919)
new_primMulNat0(xux500) → new_primPlusNat0(Zero, Succ(xux500))
new_gt0(Pos(Zero), Pos(Succ(xux197200))) → new_esEs11(Zero, xux197200)
new_primMinusNat0(Zero, Succ(xux12430)) → Neg(Succ(xux12430))
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, Zero, h, ba) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_esEs7(Succ(xux1977000), Succ(xux1972000)) → new_esEs7(xux1977000, xux1972000)
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, xux52643, xux52644, xux1958, True, h, ba) → new_mkBranchResult(xux52640, xux52641, xux52644, new_mkBranchResult(xux5260, xux5261, xux52643, xux1958, h, ba), h, ba)
new_mkVBalBranch3MkVBalBranch10(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, h, ba) → new_mkBalBranch6MkBalBranch55(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, new_lt(new_ps(new_mkBalBranch6Size_l(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), h, ba), new_mkBalBranch6Size_r(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), h, ba)), Pos(Succ(Succ(Zero)))), h, ba)
new_lt0(xux528, xux5220, app(app(ty_@2, ea), eb)) → error([])
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Succ(xux195600)), Pos(xux19550), h, ba) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_ps(Pos(xux19360), Pos(xux19350)) → Pos(new_primPlusNat0(xux19360, xux19350))
new_mkBalBranch6MkBalBranch55(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, True, h, ba) → new_mkBranch1(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), h, ba)
new_esEs9 → False
new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba) → new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_addToFM(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, h, ba) → new_addToFM_C30(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, h, ba)
new_esEs8 → True
new_gt0(Neg(Zero), Pos(Succ(xux197200))) → new_esEs5
new_mkVBalBranch3MkVBalBranch10(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, False, h, ba) → new_mkBranch2(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))), xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)
new_ps(Pos(xux19360), Neg(xux19350)) → new_primMinusNat0(xux19360, xux19350)
new_ps(Neg(xux19360), Pos(xux19350)) → new_primMinusNat0(xux19350, xux19360)
new_gt(xux1977, xux1972, ty_Int) → new_gt0(xux1977, xux1972)
new_lt0(xux528, xux5220, ty_Bool) → error([])
new_mkBalBranch6Size_r(xux5260, xux5261, xux1875, xux5264, h, ba) → new_sizeFM(xux5264, h, ba)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Succ(xux195600)), Neg(xux19550), h, ba) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_esEs10(Neg(Zero), Pos(Zero)) → new_esEs1
new_esEs10(Pos(Zero), Neg(Zero)) → new_esEs1
new_gt0(Pos(Succ(xux197700)), Pos(xux19720)) → new_esEs6(xux197700, xux19720)
new_esEs10(Neg(Succ(xux52800)), Pos(xux5190)) → new_esEs4
new_sr(Neg(xux20120)) → Neg(new_primMulNat2(xux20120))
new_primMulNat1(xux500) → new_primPlusNat0(new_primMulNat(xux500), Succ(xux500))
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Succ(xux195600)), Pos(xux19550), h, ba) → new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, xux19550, h, ba)
new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, False, de, df) → new_mkBalBranch6MkBalBranch40(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, de, df), xux1992, new_mkBalBranch6Size_r(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, de, df), de, df), new_sr0(new_mkBalBranch6Size_l(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, de, df), de, df)), de, df)
new_addToFM_C20(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, True, bb, bc) → new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, new_lt(new_ps(new_mkBalBranch6Size_l(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc), new_mkBalBranch6Size_r(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc)), Pos(Succ(Succ(Zero)))), bb, bc)
new_mkBranch(xux2028, xux2029, xux2030, xux2031, xux2032, xux2033, xux2034, xux2035, xux2036, dc, dd) → new_mkBranchResult(xux2029, xux2030, new_mkBranch0(xux2032, xux2033, xux2034, xux2035, xux2036, dc, dd), xux2031, dc, dd)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Pos(Succ(xux195500)), h, ba) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_primMulInt(xux1859) → new_primMulInt0(xux1859)
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, xux1958, False, h, ba) → new_mkBranchResult(xux5260, xux5261, xux5264, xux1958, h, ba)
new_esEs10(Pos(Zero), Neg(Succ(xux51900))) → new_esEs3
new_mkVBalBranch30(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba) → new_mkVBalBranch3MkVBalBranch20(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, h, ba)), h, ba)
new_gt0(Pos(Zero), Neg(Succ(xux197200))) → new_esEs8
new_gt(xux1977, xux1972, app(ty_Maybe, bd)) → error([])
new_lt0(xux528, xux5220, ty_@0) → error([])
new_esEs10(Neg(Zero), Neg(Zero)) → new_esEs1
new_primPlusNat0(Succ(xux1020000), Succ(xux542000)) → Succ(Succ(new_primPlusNat0(xux1020000, xux542000)))
new_esEs7(Zero, Zero) → new_esEs9
new_esEs7(Zero, Succ(xux1972000)) → new_esEs5
new_esEs4 → True
new_lt0(xux528, xux5220, ty_Int) → new_lt(xux528, xux5220)
new_esEs11(Zero, xux197700) → new_esEs5
new_primPlusNat0(Zero, Zero) → Zero
new_gt(xux1977, xux1972, ty_Double) → error([])
new_esEs6(xux197700, Zero) → new_esEs8
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, Succ(xux1955000), h, ba) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_esEs6(xux197700, Succ(xux197200)) → new_esEs7(xux197700, xux197200)
new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, EmptyFM, h, ba) → new_addToFM(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, h, ba)
new_primMinusNat0(Succ(xux129700), Zero) → Pos(Succ(xux129700))
new_primMulNat3(Succ(xux184000)) → new_primPlusNat0(new_primMulNat1(xux184000), Succ(xux184000))
new_sizeFM(EmptyFM, cf, cg) → Pos(Zero)
new_gt(xux1977, xux1972, app(ty_[], be)) → error([])
new_mkBranch1(xux1989, xux1990, xux1992, xux2013, de, df) → new_mkBranchResult(xux1989, xux1990, xux2013, xux1992, de, df)
new_esEs10(Pos(Zero), Pos(Succ(xux51900))) → new_esEs2(Zero, Succ(xux51900))
new_esEs2(Zero, Zero) → new_esEs1
new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, Succ(xux195500), h, ba) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, xux195500, h, ba)
new_mkVBalBranch1(xux528, xux529, Branch(xux52240, xux52241, xux52242, xux52243, xux52244), xux5260, xux5261, xux5262, xux5263, xux5264, h, ba) → new_mkVBalBranch30(xux528, xux529, xux52240, xux52241, xux52242, xux52243, xux52244, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba)
new_sizeFM(Branch(xux15350, xux15351, xux15352, xux15353, xux15354), cf, cg) → xux15352
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, EmptyFM, xux52644, xux1958, False, h, ba) → error([])
new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba) → new_sizeFM(Branch(xux5220, xux5221, xux5222, xux5223, xux5224), h, ba)
new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, EmptyFM, xux1958, h, ba) → error([])
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, EmptyFM, True, h, ba) → error([])
new_esEs11(Succ(xux197200), xux197700) → new_esEs7(xux197200, xux197700)
new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, False, bb, bc) → new_mkBalBranch6MkBalBranch40(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), new_mkBalBranch6Size_r(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc), new_sr0(new_mkBalBranch6Size_l(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bb, bc), xux1976, bb, bc)), bb, bc)
new_lt0(xux528, xux5220, app(ty_Maybe, dg)) → error([])
new_gt(xux1977, xux1972, ty_Bool) → error([])
new_esEs10(Neg(Zero), Pos(Succ(xux51900))) → new_esEs4
new_esEs1 → False
new_lt0(xux528, xux5220, ty_Double) → error([])
new_esEs3 → False
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_esEs7(Succ(xux1977000), Zero) → new_esEs8
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, Branch(xux526430, xux526431, xux526432, xux526433, xux526434), xux52644, xux1958, False, h, ba) → new_mkBranch(Succ(Succ(Succ(Succ(Zero)))), xux526430, xux526431, new_mkBranchResult(xux5260, xux5261, xux526433, xux1958, h, ba), Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))), xux52640, xux52641, xux526434, xux52644, h, ba)
new_addToFM_C10(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, False, de, df) → Branch(xux1994, xux1995, xux1991, xux1992, xux1993)
new_addToFM_C10(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, True, de, df) → new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, new_lt(new_ps(new_mkBalBranch6Size_l(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, de, df), de, df), new_mkBalBranch6Size_r(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, de, df), de, df)), Pos(Succ(Succ(Zero)))), de, df)
new_gt0(Neg(Succ(xux197700)), Pos(xux19720)) → new_esEs5
new_primMulNat2(Zero) → Zero
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux1956000), Zero, h, ba) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_lt0(xux528, xux5220, app(app(ty_Either, ec), ed)) → error([])
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Succ(xux195600)), Neg(xux19550), h, ba) → new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, xux19550, xux195600, h, ba)
new_mkBranchResult(xux5260, xux5261, xux5264, xux1960, h, ba) → Branch(xux5260, xux5261, new_mkBranchUnbox(xux5264, xux5260, xux1960, new_ps(new_ps(Pos(Succ(Zero)), new_sizeFM(xux1960, h, ba)), new_sizeFM(xux5264, h, ba)), h, ba), xux1960, xux5264)
new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, xux195600, h, ba) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, EmptyFM, False, h, ba) → error([])
new_lt0(xux528, xux5220, ty_Float) → error([])
new_esEs2(Succ(xux5200000000), Succ(xux18190)) → new_esEs2(xux5200000000, xux18190)
new_gt(xux1977, xux1972, app(app(ty_@2, bf), bg)) → error([])
new_gt0(Neg(Succ(xux197700)), Neg(xux19720)) → new_esEs11(xux19720, xux197700)
new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, True, de, df) → new_mkBranch1(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, de, df), de, df)
new_lt0(xux528, xux5220, ty_Ordering) → error([])
new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux195500), xux195600, h, ba) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux195500, xux195600, h, ba)
new_esEs10(Neg(Zero), Neg(Succ(xux51900))) → new_esEs2(Succ(xux51900), Zero)
new_mkVBalBranch3MkVBalBranch20(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, h, ba) → new_mkBalBranch6MkBalBranch56(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, new_lt(new_ps(new_mkBalBranch6Size_l(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, h, ba), new_mkBalBranch6Size_r(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, h, ba), xux5264, h, ba)), Pos(Succ(Succ(Zero)))), h, ba)
new_primMulNat2(Succ(xux201200)) → new_primPlusNat0(new_primMulNat0(xux201200), Succ(xux201200))
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Pos(Zero), h, ba) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, h, ba)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Pos(Succ(xux195500)), h, ba) → new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, xux195500, h, ba)
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, Branch(xux19580, xux19581, xux19582, xux19583, xux19584), True, h, ba) → new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, xux19584, new_lt(new_sizeFM(xux19584, h, ba), new_sr(new_sizeFM(xux19583, h, ba))), h, ba)
new_sr(Pos(xux20120)) → Pos(new_primMulNat2(xux20120))
new_primPlusNat0(Zero, Succ(xux542000)) → Succ(xux542000)
new_primPlusNat0(Succ(xux1020000), Zero) → Succ(xux1020000)
new_mkBalBranch6MkBalBranch55(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, False, h, ba) → new_mkBalBranch6MkBalBranch40(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), xux5223, new_mkBalBranch6Size_r(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), h, ba), new_sr0(new_mkBalBranch6Size_l(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, h, ba), h, ba)), h, ba)
new_gt0(Pos(Zero), Neg(Zero)) → new_esEs9
new_gt0(Neg(Zero), Pos(Zero)) → new_esEs9
new_mkBranch0(xux2032, xux2033, xux2034, xux2035, xux2036, dc, dd) → new_mkBranchResult(xux2033, xux2034, xux2036, xux2035, dc, dd)
new_gt(xux1977, xux1972, app(app(ty_Either, bh), ca)) → error([])
new_primMinusNat0(Succ(xux129700), Succ(xux12430)) → new_primMinusNat0(xux129700, xux12430)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Succ(x5)), Pos(x6), x7, x8)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Succ(x5)), Neg(x6), x7, x8)
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, EmptyFM, True, x4, x5)
new_ps(Neg(x0), Neg(x1))
new_gt(x0, x1, ty_@0)
new_gt(x0, x1, app(app(ty_@2, x2), x3))
new_gt0(Pos(Zero), Pos(Succ(x0)))
new_lt0(x0, x1, ty_Float)
new_addToFM_C(EmptyFM, x0, x1, x2, x3)
new_mkVBalBranch(x0, x1, x2, x3, x4, x5, x6, Branch(x7, x8, x9, x10, x11), x12, x13)
new_gt0(Neg(Zero), Pos(Succ(x0)))
new_gt0(Pos(Zero), Neg(Succ(x0)))
new_gt(x0, x1, ty_Char)
new_gt(x0, x1, ty_Ordering)
new_gt0(Pos(Succ(x0)), Pos(x1))
new_primMinusNat0(Zero, Zero)
new_mkVBalBranch1(x0, x1, Branch(x2, x3, x4, x5, x6), x7, x8, x9, x10, x11, x12, x13)
new_esEs5
new_emptyFM(x0, x1)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Succ(x5), Succ(x6), x7, x8)
new_mkBalBranch6MkBalBranch55(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
new_lt0(x0, x1, app(ty_[], x2))
new_mkBalBranch6MkBalBranch47(x0, x1, x2, x3, x4, x5, x6)
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_primMulNat3(Succ(x0))
new_esEs7(Zero, Zero)
new_mkBranchResult(x0, x1, x2, x3, x4, x5)
new_mkBranch1(x0, x1, x2, x3, x4, x5)
new_esEs10(Neg(Zero), Neg(Succ(x0)))
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, EmptyFM, x6, x7, False, x8, x9)
new_mkBalBranch6MkBalBranch55(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, True, x11, x12)
new_esEs7(Succ(x0), Succ(x1))
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Succ(x5)), Neg(x6), x7, x8)
new_lt0(x0, x1, ty_@0)
new_mkVBalBranch3MkVBalBranch10(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Pos(Zero), x5, x6)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Neg(Zero), x5, x6)
new_gt(x0, x1, app(ty_[], x2))
new_gt(x0, x1, ty_Bool)
new_primMulNat(x0)
new_ps(Neg(x0), Pos(x1))
new_ps(Pos(x0), Neg(x1))
new_lt0(x0, x1, app(app(ty_Either, x2), x3))
new_mkBalBranch6MkBalBranch41(x0, x1, x2, x3, x4, x5, Succ(x6), x7, x8)
new_sizeFM(EmptyFM, x0, x1)
new_addToFM_C30(x0, x1, x2, x3, x4, x5, x6, x7, x8)
new_mkBalBranch6MkBalBranch52(x0, x1, x2, x3, x4, x5, True, x6, x7)
new_gt(x0, x1, app(app(ty_Either, x2), x3))
new_gt(x0, x1, app(ty_Maybe, x2))
new_primMulInt0(Neg(x0))
new_primMulNat2(Succ(x0))
new_mkBalBranch6MkBalBranch42(x0, x1, x2, EmptyFM, x3, x4, x5)
new_mkBranch2(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)
new_gt(x0, x1, ty_Integer)
new_mkBalBranch6MkBalBranch56(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, True, x11, x12)
new_mkBalBranch6MkBalBranch45(x0, x1, x2, x3, x4, x5, x6)
new_lt0(x0, x1, ty_Ordering)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Succ(x5), Zero, x6, x7)
new_mkVBalBranch30(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
new_gt(x0, x1, ty_Double)
new_mkVBalBranch3MkVBalBranch20(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_lt0(x0, x1, ty_Char)
new_mkBalBranch6MkBalBranch44(x0, x1, x2, x3, x4, x5, x6)
new_primPlusNat0(Succ(x0), Succ(x1))
new_lt0(x0, x1, ty_Bool)
new_esEs8
new_esEs6(x0, Succ(x1))
new_esEs9
new_primMinusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Succ(x0))
new_esEs10(Pos(Zero), Neg(Zero))
new_esEs10(Neg(Zero), Pos(Zero))
new_primMulNat0(x0)
new_lt0(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(Pos(Succ(x0)), Neg(x1))
new_esEs10(Neg(Succ(x0)), Pos(x1))
new_esEs3
new_gt0(Neg(Succ(x0)), Pos(x1))
new_gt0(Pos(Succ(x0)), Neg(x1))
new_mkBalBranch6Size_r(x0, x1, x2, x3, x4, x5)
new_mkBranch0(x0, x1, x2, x3, x4, x5, x6)
new_esEs7(Zero, Succ(x0))
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Succ(x5)), Pos(x6), x7, x8)
new_mkVBalBranch3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_mkVBalBranch1(x0, x1, EmptyFM, x2, x3, x4, x5, x6, x7, x8)
new_mkVBalBranch3Size_r(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_sr0(x0)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, EmptyFM, False, x8, x9)
new_lt0(x0, x1, app(app(ty_@2, x2), x3))
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Pos(Succ(x5)), x6, x7)
new_gt0(Pos(Zero), Neg(Zero))
new_gt0(Neg(Zero), Pos(Zero))
new_esEs4
new_primMulInt(x0)
new_primPlusNat0(Succ(x0), Zero)
new_esEs7(Succ(x0), Zero)
new_esEs10(Neg(Succ(x0)), Neg(x1))
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Zero, Succ(x5), x6, x7)
new_lt(x0, x1)
new_mkVBalBranch3MkVBalBranch20(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, True, x12, x13)
new_lt0(x0, x1, app(ty_Ratio, x2))
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, Branch(x6, x7, x8, x9, x10), x11, x12, False, x13, x14)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Neg(Succ(x5)), x6, x7)
new_esEs10(Pos(Zero), Pos(Succ(x0)))
new_mkBalBranch6MkBalBranch52(x0, x1, x2, x3, x4, x5, False, x6, x7)
new_gt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, Branch(x8, x9, x10, x11, x12), False, x13, x14)
new_mkBalBranch6MkBalBranch43(x0, x1, x2, x3, x4, Succ(x5), x6, x7, x8)
new_ps(Pos(x0), Pos(x1))
new_lt0(x0, x1, ty_Double)
new_lt0(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Zero, Zero)
new_gt(x0, x1, app(ty_Ratio, x2))
new_esEs11(Zero, x0)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Zero, Zero, x5, x6)
new_mkBalBranch6MkBalBranch41(x0, x1, x2, x3, x4, x5, Zero, x6, x7)
new_primMulInt0(Pos(x0))
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_esEs10(Neg(Zero), Neg(Zero))
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Pos(Zero), x5, x6)
new_esEs6(x0, Zero)
new_gt0(Neg(Zero), Neg(Zero))
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs2(Zero, Succ(x0))
new_primMinusNat0(Succ(x0), Zero)
new_mkBalBranch6Size_l(x0, x1, x2, x3, x4, x5)
new_esEs11(Succ(x0), x1)
new_esEs10(Neg(Zero), Pos(Succ(x0)))
new_esEs10(Pos(Succ(x0)), Pos(x1))
new_esEs10(Pos(Zero), Neg(Succ(x0)))
new_primMulNat2(Zero)
new_addToFM_C(Branch(x0, x1, x2, x3, x4), x5, x6, x7, x8)
new_esEs2(Succ(x0), Zero)
new_mkVBalBranch3MkVBalBranch10(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, True, x12, x13)
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, Branch(x4, x5, x6, x7, x8), True, x9, x10)
new_mkBalBranch6MkBalBranch43(x0, x1, x2, x3, x4, Zero, x5, x6, x7)
new_sr(Pos(x0))
new_lt0(x0, x1, ty_Int)
new_gt0(Neg(Zero), Neg(Succ(x0)))
new_addToFM(x0, x1, x2, x3, x4, x5, x6, x7, x8)
new_gt0(Pos(Zero), Pos(Zero))
new_mkBalBranch6MkBalBranch51(x0, x1, x2, x3, x4, x5, True, x6, x7)
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_esEs2(Succ(x0), Succ(x1))
new_primMulNat1(x0)
new_esEs10(Pos(Zero), Pos(Zero))
new_sr(Neg(x0))
new_esEs1
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Neg(Zero), x5, x6)
new_mkBalBranch6MkBalBranch56(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
new_primMinusNat0(Succ(x0), Succ(x1))
new_mkBranch(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
new_lt0(x0, x1, ty_Integer)
new_gt(x0, x1, ty_Int)
new_mkVBalBranch(x0, x1, x2, x3, x4, x5, x6, EmptyFM, x7, x8)
new_mkBranchUnbox(x0, x1, x2, x3, x4, x5)
new_primMulNat3(Zero)
new_mkBalBranch6MkBalBranch42(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, x9, x10)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Neg(Succ(x5)), x6, x7)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Pos(Succ(x5)), x6, x7)
new_gt0(Neg(Succ(x0)), Neg(x1))
new_mkBalBranch6MkBalBranch51(x0, x1, x2, x3, x4, x5, False, x6, x7)
new_esEs2(Zero, Zero)
new_gt(x0, x1, ty_Float)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
new_splitLT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitLT20(xux3000, xux31, xux32, xux33, xux34, xux4000, xux3000, xux4000, ba)
new_splitLT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitLT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, ba)
new_splitLT10(xux861, xux862, xux863, xux864, xux865, xux866, Succ(xux8670), Zero, bd) → new_splitLT4(xux865, xux866, bd)
new_splitLT22(xux371, xux372, xux373, xux374, xux375, xux376, bc) → new_splitLT10(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux371), Succ(xux376), bc)
new_splitLT3(Pos(xux300), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Neg(Succ(xux4000)), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Zero, Succ(xux3690), bb) → new_splitLT(xux365, xux367, bb)
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Zero, Zero, bb) → new_splitLT21(xux362, xux363, xux364, xux365, xux366, xux367, bb)
new_splitLT3(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitLT4(xux33, xux4000, ba)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Zero, Zero, bc) → new_splitLT22(xux371, xux372, xux373, xux374, xux375, xux376, bc)
new_splitLT1(xux852, xux853, xux854, xux855, xux856, xux857, Succ(xux8580), Zero, h) → new_splitLT(xux856, xux857, h)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux3770), Succ(xux3780), bc) → new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, xux3770, xux3780, bc)
new_splitLT3(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitLT(xux34, xux4000, ba)
new_splitLT10(xux861, xux862, xux863, xux864, xux865, xux866, Succ(xux8670), Succ(xux8680), bd) → new_splitLT10(xux861, xux862, xux863, xux864, xux865, xux866, xux8670, xux8680, bd)
new_splitLT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), ba) → new_splitLT5(xux34, ba)
new_splitLT4(Branch(xux330, xux331, xux332, xux333, xux334), xux4000, ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitLT3(Pos(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Pos(Zero), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Pos(Zero), ba)
new_splitLT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitLT0(Branch(xux330, xux331, xux332, xux333, xux334), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Pos(Zero), ba)
new_splitLT5(Branch(xux330, xux331, xux332, xux333, xux334), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Zero), ba)
new_splitLT1(xux852, xux853, xux854, xux855, xux856, xux857, Succ(xux8580), Succ(xux8590), h) → new_splitLT1(xux852, xux853, xux854, xux855, xux856, xux857, xux8580, xux8590, h)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Zero, Succ(xux3780), bc) → new_splitLT4(xux374, xux376, bc)
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux3680), Succ(xux3690), bb) → new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, xux3680, xux3690, bb)
new_splitLT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), ba) → new_splitLT0(xux34, ba)
new_splitLT3(Neg(xux300), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Pos(Succ(xux4000)), ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux3680), Zero, bb) → new_splitLT1(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux367), Succ(xux362), bb)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux3770), Zero, bc) → new_splitLT10(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux371), Succ(xux376), bc)
new_splitLT21(xux362, xux363, xux364, xux365, xux366, xux367, bb) → new_splitLT1(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux367), Succ(xux362), bb)
new_splitLT3(Pos(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Neg(Zero), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Zero), ba)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_splitLT3(Pos(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Pos(Zero), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Pos(Zero), ba)
new_splitLT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), ba) → new_splitLT0(xux34, ba)
new_splitLT0(Branch(xux330, xux331, xux332, xux333, xux334), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Pos(Zero), ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_splitLT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), ba) → new_splitLT5(xux34, ba)
new_splitLT5(Branch(xux330, xux331, xux332, xux333, xux334), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Zero), ba)
new_splitLT3(Pos(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Neg(Zero), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Zero), ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux3680), Succ(xux3690), bb) → new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, xux3680, xux3690, bb)
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Zero, Zero, bb) → new_splitLT21(xux362, xux363, xux364, xux365, xux366, xux367, bb)
new_splitLT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitLT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, ba)
new_splitLT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitLT3(Neg(xux300), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Pos(Succ(xux4000)), ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux3680), Zero, bb) → new_splitLT1(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux367), Succ(xux362), bb)
new_splitLT1(xux852, xux853, xux854, xux855, xux856, xux857, Succ(xux8580), Zero, h) → new_splitLT(xux856, xux857, h)
new_splitLT2(xux362, xux363, xux364, xux365, xux366, xux367, Zero, Succ(xux3690), bb) → new_splitLT(xux365, xux367, bb)
new_splitLT3(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitLT(xux34, xux4000, ba)
new_splitLT1(xux852, xux853, xux854, xux855, xux856, xux857, Succ(xux8580), Succ(xux8590), h) → new_splitLT1(xux852, xux853, xux854, xux855, xux856, xux857, xux8580, xux8590, h)
new_splitLT21(xux362, xux363, xux364, xux365, xux366, xux367, bb) → new_splitLT1(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux367), Succ(xux362), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
new_splitLT10(xux861, xux862, xux863, xux864, xux865, xux866, Succ(xux8670), Succ(xux8680), bd) → new_splitLT10(xux861, xux862, xux863, xux864, xux865, xux866, xux8670, xux8680, bd)
new_splitLT4(Branch(xux330, xux331, xux332, xux333, xux334), xux4000, ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitLT3(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitLT4(xux33, xux4000, ba)
new_splitLT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitLT20(xux3000, xux31, xux32, xux33, xux34, xux4000, xux3000, xux4000, ba)
new_splitLT10(xux861, xux862, xux863, xux864, xux865, xux866, Succ(xux8670), Zero, bd) → new_splitLT4(xux865, xux866, bd)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Zero, Zero, bc) → new_splitLT22(xux371, xux372, xux373, xux374, xux375, xux376, bc)
new_splitLT3(Pos(xux300), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Neg(Succ(xux4000)), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitLT22(xux371, xux372, xux373, xux374, xux375, xux376, bc) → new_splitLT10(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux371), Succ(xux376), bc)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux3770), Succ(xux3780), bc) → new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, xux3770, xux3780, bc)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux3770), Zero, bc) → new_splitLT10(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux371), Succ(xux376), bc)
new_splitLT20(xux371, xux372, xux373, xux374, xux375, xux376, Zero, Succ(xux3780), bc) → new_splitLT4(xux374, xux376, bc)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Zero, Zero, bc) → new_splitGT22(xux353, xux354, xux355, xux356, xux357, xux358, bc)
new_splitGT3(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitGT4(xux33, xux4000, ba)
new_splitGT3(Pos(xux300), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Neg(Succ(xux4000)), ba) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Zero, Succ(xux3510), bb) → new_splitGT1(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux349), Succ(xux344), bb)
new_splitGT3(Neg(Succ(xux3000)), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Neg(Zero), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Neg(Zero), ba)
new_splitGT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), ba) → new_splitGT0(xux33, ba)
new_splitGT3(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitGT(xux34, xux4000, ba)
new_splitGT22(xux353, xux354, xux355, xux356, xux357, xux358, bc) → new_splitGT10(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux353), Succ(xux358), bc)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux3500), Succ(xux3510), bb) → new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, xux3500, xux3510, bb)
new_splitGT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), ba) → new_splitGT5(xux33, ba)
new_splitGT1(xux834, xux835, xux836, xux837, xux838, xux839, Succ(xux8400), Succ(xux8410), h) → new_splitGT1(xux834, xux835, xux836, xux837, xux838, xux839, xux8400, xux8410, h)
new_splitGT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitGT20(xux3000, xux31, xux32, xux33, xux34, xux4000, xux3000, xux4000, ba)
new_splitGT3(Neg(xux300), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Pos(Succ(xux4000)), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux3500), Zero, bb) → new_splitGT(xux348, xux349, bb)
new_splitGT10(xux843, xux844, xux845, xux846, xux847, xux848, Succ(xux8490), Succ(xux8500), bd) → new_splitGT10(xux843, xux844, xux845, xux846, xux847, xux848, xux8490, xux8500, bd)
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Zero, Succ(xux3600), bc) → new_splitGT10(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux353), Succ(xux358), bc)
new_splitGT4(Branch(xux330, xux331, xux332, xux333, xux334), xux4000, ba) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitGT0(Branch(xux340, xux341, xux342, xux343, xux344), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Zero), ba)
new_splitGT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitGT5(Branch(xux340, xux341, xux342, xux343, xux344), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Neg(Zero), ba)
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux3590), Succ(xux3600), bc) → new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, xux3590, xux3600, bc)
new_splitGT3(Neg(Succ(xux3000)), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Pos(Zero), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Zero), ba)
new_splitGT1(xux834, xux835, xux836, xux837, xux838, xux839, Zero, Succ(xux8410), h) → new_splitGT(xux837, xux839, h)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Zero, Zero, bb) → new_splitGT21(xux344, xux345, xux346, xux347, xux348, xux349, bb)
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux3590), Zero, bc) → new_splitGT4(xux357, xux358, bc)
new_splitGT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitGT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, ba)
new_splitGT21(xux344, xux345, xux346, xux347, xux348, xux349, bb) → new_splitGT1(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux349), Succ(xux344), bb)
new_splitGT10(xux843, xux844, xux845, xux846, xux847, xux848, Zero, Succ(xux8500), bd) → new_splitGT4(xux846, xux848, bd)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_splitGT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), ba) → new_splitGT0(xux33, ba)
new_splitGT0(Branch(xux340, xux341, xux342, xux343, xux344), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Zero), ba)
new_splitGT3(Neg(Succ(xux3000)), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Pos(Zero), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Zero), ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_splitGT1(xux834, xux835, xux836, xux837, xux838, xux839, Zero, Succ(xux8410), h) → new_splitGT(xux837, xux839, h)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Zero, Succ(xux3510), bb) → new_splitGT1(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux349), Succ(xux344), bb)
new_splitGT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitGT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, ba)
new_splitGT3(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), ba) → new_splitGT(xux34, xux4000, ba)
new_splitGT21(xux344, xux345, xux346, xux347, xux348, xux349, bb) → new_splitGT1(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux349), Succ(xux344), bb)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Zero, Zero, bb) → new_splitGT21(xux344, xux345, xux346, xux347, xux348, xux349, bb)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux3500), Succ(xux3510), bb) → new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, xux3500, xux3510, bb)
new_splitGT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitGT1(xux834, xux835, xux836, xux837, xux838, xux839, Succ(xux8400), Succ(xux8410), h) → new_splitGT1(xux834, xux835, xux836, xux837, xux838, xux839, xux8400, xux8410, h)
new_splitGT3(Neg(xux300), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Pos(Succ(xux4000)), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), ba)
new_splitGT2(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux3500), Zero, bb) → new_splitGT(xux348, xux349, bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
new_splitGT3(Neg(Succ(xux3000)), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Neg(Zero), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Neg(Zero), ba)
new_splitGT3(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), ba) → new_splitGT5(xux33, ba)
new_splitGT5(Branch(xux340, xux341, xux342, xux343, xux344), ba) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Neg(Zero), ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Zero, Zero, bc) → new_splitGT22(xux353, xux354, xux355, xux356, xux357, xux358, bc)
new_splitGT3(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitGT4(xux33, xux4000, ba)
new_splitGT10(xux843, xux844, xux845, xux846, xux847, xux848, Succ(xux8490), Succ(xux8500), bd) → new_splitGT10(xux843, xux844, xux845, xux846, xux847, xux848, xux8490, xux8500, bd)
new_splitGT3(Pos(xux300), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Neg(Succ(xux4000)), ba) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Zero, Succ(xux3600), bc) → new_splitGT10(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux353), Succ(xux358), bc)
new_splitGT4(Branch(xux330, xux331, xux332, xux333, xux334), xux4000, ba) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), ba)
new_splitGT22(xux353, xux354, xux355, xux356, xux357, xux358, bc) → new_splitGT10(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux353), Succ(xux358), bc)
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux3590), Zero, bc) → new_splitGT4(xux357, xux358, bc)
new_splitGT10(xux843, xux844, xux845, xux846, xux847, xux848, Zero, Succ(xux8500), bd) → new_splitGT4(xux846, xux848, bd)
new_splitGT3(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), ba) → new_splitGT20(xux3000, xux31, xux32, xux33, xux34, xux4000, xux3000, xux4000, ba)
new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux3590), Succ(xux3600), bc) → new_splitGT20(xux353, xux354, xux355, xux356, xux357, xux358, xux3590, xux3600, bc)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
new_plusFM(Branch(xux30, xux31, xux32, xux33, xux34), Branch(xux40, xux41, xux42, xux43, xux44), h) → new_plusFM(new_splitGT30(xux30, xux31, xux32, xux33, xux34, xux40, h), xux44, h)
new_plusFM(Branch(xux30, xux31, xux32, xux33, xux34), Branch(xux40, xux41, xux42, xux43, xux44), h) → new_plusFM(new_splitLT30(xux30, xux31, xux32, xux33, xux34, xux40, h), xux43, h)
new_esEs10(Pos(Zero), Pos(Zero)) → new_esEs1
new_gt(xux1977, xux1972, ty_Integer) → error([])
new_splitLT11(xux861, xux862, xux863, xux864, xux865, xux866, Succ(xux8670), Succ(xux8680), dc) → new_splitLT11(xux861, xux862, xux863, xux864, xux865, xux866, xux8670, xux8680, dc)
new_splitLT25(xux371, xux372, xux373, xux374, xux375, xux376, Zero, Succ(xux3780), cg) → new_splitLT6(xux374, xux376, cg)
new_lt0(xux528, xux5220, ty_Char) → error([])
new_mkBalBranch6Size_l(xux5260, xux5261, xux1866, xux5264, ba, bb) → new_sizeFM(xux1866, ba, bb)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Pos(Zero), ba, bb) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Neg(Zero), ba, bb) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_addToFM_C(Branch(xux19750, xux19751, xux19752, xux19753, xux19754), xux1977, xux1978, bc, bd) → new_addToFM_C30(xux19750, xux19751, xux19752, xux19753, xux19754, xux1977, xux1978, bc, bd)
new_mkBalBranch6MkBalBranch56(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, False, ba, bb) → new_mkBalBranch6MkBalBranch40(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, ba, bb), xux5264, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, ba, bb), new_mkBalBranch6Size_r(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, ba, bb), xux5264, ba, bb), new_sr0(new_mkBalBranch6Size_l(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, ba, bb), xux5264, ba, bb)), ba, bb)
new_splitLT26(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux3680), Succ(xux3690), db) → new_splitLT26(xux362, xux363, xux364, xux365, xux366, xux367, xux3680, xux3690, db)
new_esEs2(Zero, Succ(xux18190)) → new_esEs4
new_splitGT30(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), h) → new_splitGT8(xux34, xux4000, h)
new_esEs2(Succ(xux5200000000), Zero) → new_esEs3
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Neg(Succ(xux195500)), ba, bb) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb) → new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, xux1958, new_gt0(new_mkBalBranch6Size_l(xux5260, xux5261, xux1959, xux5264, ba, bb), new_sr0(new_mkBalBranch6Size_r(xux5260, xux5261, xux1959, xux5264, ba, bb))), ba, bb)
new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb) → new_sizeFM(Branch(xux5260, xux5261, xux5262, xux5263, xux5264), ba, bb)
new_addToFM_C20(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, False, bc, bd) → new_addToFM_C10(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, new_gt(xux1977, xux1972, bc), bc, bd)
new_esEs10(Pos(Succ(xux52800)), Neg(xux5190)) → new_esEs3
new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, Branch(xux52640, xux52641, xux52642, xux52643, xux52644), xux1958, ba, bb) → new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, xux52643, xux52644, xux1958, new_lt(new_sizeFM(xux52643, ba, bb), new_sr(new_sizeFM(xux52644, ba, bb))), ba, bb)
new_splitLT12(xux852, xux853, xux854, xux855, xux856, xux857, Zero, Succ(xux8590), dd) → new_splitLT14(xux852, xux853, xux854, xux855, xux856, xux857, dd)
new_primMulInt0(Neg(xux18400)) → Neg(new_primMulNat3(xux18400))
new_gt(xux1977, xux1972, app(ty_Ratio, cf)) → error([])
new_splitLT7(EmptyFM, xux4000, h) → new_emptyFM0(h)
new_emptyFM(bc, bd) → EmptyFM
new_gt0(Pos(Succ(xux197700)), Neg(xux19720)) → new_esEs8
new_primMulInt0(Pos(xux18400)) → Pos(new_primMulNat3(xux18400))
new_lt0(xux528, xux5220, app(ty_[], eh)) → error([])
new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, Zero, ba, bb) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_mkBranch2(xux1938, xux1939, xux1940, xux1941, xux1942, xux1943, xux1944, xux1945, xux1946, xux1947, xux1948, xux1949, xux1950, dh, ea) → new_mkBranchResult(xux1939, xux1940, Branch(xux1946, xux1947, xux1948, xux1949, xux1950), Branch(xux1941, xux1942, xux1943, xux1944, xux1945), dh, ea)
new_mkVBalBranch1(xux528, xux529, EmptyFM, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb) → new_addToFM(xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, ba, bb)
new_addToFM_C30(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, ba, bb) → new_addToFM_C20(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, new_lt0(xux528, xux5220, ba), ba, bb)
new_addToFM_C4(Branch(xux50, xux51, xux52, xux53, xux54), xux40, xux41, h) → new_addToFM_C20(xux50, xux51, xux52, xux53, xux54, xux40, xux41, new_lt(xux40, xux50), ty_Int, h)
new_splitGT12(xux834, xux835, xux836, xux837, xux838, xux839, de) → xux838
new_lt0(xux528, xux5220, app(app(app(ty_@3, ff), fg), fh)) → error([])
new_splitLT30(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), h) → new_mkVBalBranch4(Neg(Succ(xux3000)), xux31, xux33, new_splitLT9(xux34, h), h)
new_primMulNat3(Zero) → Zero
new_splitGT13(xux843, xux844, xux845, xux846, xux847, xux848, Zero, Succ(xux8500), gb) → new_mkVBalBranch4(Neg(Succ(xux843)), xux844, new_splitGT6(xux846, xux848, gb), xux847, gb)
new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb) → new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_primMulNat0(xux500) → new_primPlusNat0(Zero, Succ(xux500))
new_esEs7(Succ(xux1977000), Succ(xux1972000)) → new_esEs7(xux1977000, xux1972000)
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, xux52643, xux52644, xux1958, True, ba, bb) → new_mkBranchResult(xux52640, xux52641, xux52644, new_mkBranchResult(xux5260, xux5261, xux52643, xux1958, ba, bb), ba, bb)
new_splitLT23(xux371, xux372, xux373, xux374, xux375, xux376, cg) → new_splitLT11(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux371), Succ(xux376), cg)
new_mkVBalBranch3MkVBalBranch10(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, ba, bb) → new_mkBalBranch6MkBalBranch55(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, new_lt(new_ps(new_mkBalBranch6Size_l(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb), ba, bb), new_mkBalBranch6Size_r(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb), ba, bb)), Pos(Succ(Succ(Zero)))), ba, bb)
new_ps(Pos(xux19360), Pos(xux19350)) → Pos(new_primPlusNat0(xux19360, xux19350))
new_splitGT25(xux344, xux345, xux346, xux347, xux348, xux349, eb) → new_splitGT11(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux349), Succ(xux344), eb)
new_splitLT12(xux852, xux853, xux854, xux855, xux856, xux857, Zero, Zero, dd) → new_splitLT14(xux852, xux853, xux854, xux855, xux856, xux857, dd)
new_splitLT25(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux3770), Succ(xux3780), cg) → new_splitLT25(xux371, xux372, xux373, xux374, xux375, xux376, xux3770, xux3780, cg)
new_mkBalBranch6MkBalBranch55(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, True, ba, bb) → new_mkBranch1(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb), ba, bb)
new_splitLT8(Branch(xux330, xux331, xux332, xux333, xux334), h) → new_splitLT30(xux330, xux331, xux332, xux333, xux334, Pos(Zero), h)
new_splitGT13(xux843, xux844, xux845, xux846, xux847, xux848, Succ(xux8490), Succ(xux8500), gb) → new_splitGT13(xux843, xux844, xux845, xux846, xux847, xux848, xux8490, xux8500, gb)
new_esEs9 → False
new_splitLT30(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), h) → new_splitLT6(xux33, xux4000, h)
new_addToFM(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, ba, bb) → new_addToFM_C30(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, ba, bb)
new_splitGT24(xux353, xux354, xux355, xux356, xux357, xux358, da) → new_splitGT13(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux353), Succ(xux358), da)
new_splitGT23(xux353, xux354, xux355, xux356, xux357, xux358, Zero, Zero, da) → new_splitGT24(xux353, xux354, xux355, xux356, xux357, xux358, da)
new_lt0(xux528, xux5220, ty_Bool) → error([])
new_gt(xux1977, xux1972, ty_Int) → new_gt0(xux1977, xux1972)
new_esEs10(Neg(Zero), Pos(Zero)) → new_esEs1
new_esEs10(Pos(Zero), Neg(Zero)) → new_esEs1
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Succ(xux195600)), Pos(xux19550), ba, bb) → new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, xux19550, ba, bb)
new_primMulNat1(xux500) → new_primPlusNat0(new_primMulNat(xux500), Succ(xux500))
new_addToFM_C20(xux1972, xux1973, xux1974, xux1975, xux1976, xux1977, xux1978, True, bc, bd) → new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, new_lt(new_ps(new_mkBalBranch6Size_l(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bc, bd), xux1976, bc, bd), new_mkBalBranch6Size_r(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bc, bd), xux1976, bc, bd)), Pos(Succ(Succ(Zero)))), bc, bd)
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, xux1958, False, ba, bb) → new_mkBranchResult(xux5260, xux5261, xux5264, xux1958, ba, bb)
new_mkVBalBranch30(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, ba, bb) → new_mkVBalBranch3MkVBalBranch20(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, ba, bb)), new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, ba, bb)), ba, bb)
new_splitLT24(xux362, xux363, xux364, xux365, xux366, xux367, db) → new_splitLT12(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux367), Succ(xux362), db)
new_esEs4 → True
new_esEs11(Zero, xux197700) → new_esEs5
new_primPlusNat0(Zero, Zero) → Zero
new_splitLT12(xux852, xux853, xux854, xux855, xux856, xux857, Succ(xux8580), Zero, dd) → new_mkVBalBranch4(Pos(Succ(xux852)), xux853, xux855, new_splitLT7(xux856, xux857, dd), dd)
new_splitGT8(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, h) → new_splitGT30(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), h)
new_splitGT30(Neg(Zero), xux31, xux32, xux33, xux34, Pos(Zero), h) → xux34
new_splitGT30(Pos(Zero), xux31, xux32, xux33, xux34, Neg(Zero), h) → xux34
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, Succ(xux1955000), ba, bb) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_esEs6(xux197700, Succ(xux197200)) → new_esEs7(xux197700, xux197200)
new_splitLT11(xux861, xux862, xux863, xux864, xux865, xux866, Zero, Zero, dc) → new_splitLT13(xux861, xux862, xux863, xux864, xux865, xux866, dc)
new_splitLT26(xux362, xux363, xux364, xux365, xux366, xux367, Zero, Zero, db) → new_splitLT24(xux362, xux363, xux364, xux365, xux366, xux367, db)
new_gt(xux1977, xux1972, app(ty_[], bf)) → error([])
new_splitGT26(xux344, xux345, xux346, xux347, xux348, xux349, Zero, Succ(xux3510), eb) → new_splitGT25(xux344, xux345, xux346, xux347, xux348, xux349, eb)
new_mkBranch1(xux1989, xux1990, xux1992, xux2013, ee, ef) → new_mkBranchResult(xux1989, xux1990, xux2013, xux1992, ee, ef)
new_splitLT30(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), h) → new_splitLT26(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, h)
new_mkVBalBranch1(xux528, xux529, Branch(xux52240, xux52241, xux52242, xux52243, xux52244), xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb) → new_mkVBalBranch30(xux528, xux529, xux52240, xux52241, xux52242, xux52243, xux52244, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb)
new_sizeFM(Branch(xux15350, xux15351, xux15352, xux15353, xux15354), df, dg) → xux15352
new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb) → new_sizeFM(Branch(xux5220, xux5221, xux5222, xux5223, xux5224), ba, bb)
new_splitGT26(xux344, xux345, xux346, xux347, xux348, xux349, Zero, Zero, eb) → new_splitGT25(xux344, xux345, xux346, xux347, xux348, xux349, eb)
new_splitLT9(Branch(xux330, xux331, xux332, xux333, xux334), h) → new_splitLT30(xux330, xux331, xux332, xux333, xux334, Neg(Zero), h)
new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, EmptyFM, xux1958, ba, bb) → error([])
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, EmptyFM, True, ba, bb) → error([])
new_splitGT30(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), h) → new_splitGT26(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, h)
new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, False, bc, bd) → new_mkBalBranch6MkBalBranch40(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bc, bd), xux1976, new_addToFM_C(xux1975, xux1977, xux1978, bc, bd), new_mkBalBranch6Size_r(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bc, bd), xux1976, bc, bd), new_sr0(new_mkBalBranch6Size_l(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bc, bd), xux1976, bc, bd)), bc, bd)
new_mkVBalBranch4(xux40, xux41, Branch(xux60, xux61, xux62, xux63, xux64), Branch(xux50, xux51, xux52, xux53, xux54), h) → new_mkVBalBranch3MkVBalBranch20(xux60, xux61, xux62, xux63, xux64, xux50, xux51, xux52, xux53, xux54, xux40, xux41, new_lt(new_sr0(new_sizeFM(Branch(xux60, xux61, xux62, xux63, xux64), ty_Int, h)), new_sizeFM(Branch(xux50, xux51, xux52, xux53, xux54), ty_Int, h)), ty_Int, h)
new_gt(xux1977, xux1972, ty_Bool) → error([])
new_esEs10(Neg(Zero), Pos(Succ(xux51900))) → new_esEs4
new_esEs1 → False
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_esEs7(Succ(xux1977000), Zero) → new_esEs8
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, Branch(xux526430, xux526431, xux526432, xux526433, xux526434), xux52644, xux1958, False, ba, bb) → new_mkBranch(Succ(Succ(Succ(Succ(Zero)))), xux526430, xux526431, new_mkBranchResult(xux5260, xux5261, xux526433, xux1958, ba, bb), Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))), xux52640, xux52641, xux526434, xux52644, ba, bb)
new_gt0(Neg(Succ(xux197700)), Pos(xux19720)) → new_esEs5
new_splitLT13(xux861, xux862, xux863, xux864, xux865, xux866, dc) → xux864
new_lt0(xux528, xux5220, app(app(ty_Either, fc), fd)) → error([])
new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, xux195600, ba, bb) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_mkBranchResult(xux5260, xux5261, xux5264, xux1960, ba, bb) → Branch(xux5260, xux5261, new_mkBranchUnbox(xux5264, xux5260, xux1960, new_ps(new_ps(Pos(Succ(Zero)), new_sizeFM(xux1960, ba, bb)), new_sizeFM(xux5264, ba, bb)), ba, bb), xux1960, xux5264)
new_splitLT8(EmptyFM, h) → new_emptyFM0(h)
new_splitGT30(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), h) → new_mkVBalBranch4(Pos(Succ(xux3000)), xux31, new_splitGT7(xux33, h), xux34, h)
new_splitGT30(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), h) → new_splitGT23(xux3000, xux31, xux32, xux33, xux34, xux4000, xux3000, xux4000, h)
new_lt0(xux528, xux5220, ty_Float) → error([])
new_gt(xux1977, xux1972, app(app(ty_@2, bg), bh)) → error([])
new_splitLT30(Pos(xux300), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), h) → new_splitLT6(xux33, xux4000, h)
new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux195500), xux195600, ba, bb) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux195500, xux195600, ba, bb)
new_mkVBalBranch3MkVBalBranch20(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, True, ba, bb) → new_mkBalBranch6MkBalBranch56(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, new_lt(new_ps(new_mkBalBranch6Size_l(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, ba, bb), xux5264, ba, bb), new_mkBalBranch6Size_r(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, ba, bb), xux5264, ba, bb)), Pos(Succ(Succ(Zero)))), ba, bb)
new_splitLT30(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), h) → new_mkVBalBranch4(Neg(Succ(xux3000)), xux31, xux33, new_splitLT8(xux34, h), h)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Pos(Zero), ba, bb) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_primMulNat2(Succ(xux201200)) → new_primPlusNat0(new_primMulNat0(xux201200), Succ(xux201200))
new_mkBalBranch6MkBalBranch3(xux5260, xux5261, xux1959, xux5264, Branch(xux19580, xux19581, xux19582, xux19583, xux19584), True, ba, bb) → new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, xux19584, new_lt(new_sizeFM(xux19584, ba, bb), new_sr(new_sizeFM(xux19583, ba, bb))), ba, bb)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Zero), Pos(Succ(xux195500)), ba, bb) → new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, xux195500, ba, bb)
new_sr(Pos(xux20120)) → Pos(new_primMulNat2(xux20120))
new_splitLT30(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Zero), h) → xux33
new_splitLT26(xux362, xux363, xux364, xux365, xux366, xux367, Zero, Succ(xux3690), db) → new_splitLT7(xux365, xux367, db)
new_splitGT30(Pos(xux300), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), h) → new_mkVBalBranch4(Pos(xux300), xux31, new_splitGT6(xux33, xux4000, h), xux34, h)
new_mkBranch0(xux2032, xux2033, xux2034, xux2035, xux2036, ec, ed) → new_mkBranchResult(xux2033, xux2034, xux2036, xux2035, ec, ed)
new_splitLT11(xux861, xux862, xux863, xux864, xux865, xux866, Zero, Succ(xux8680), dc) → new_splitLT13(xux861, xux862, xux863, xux864, xux865, xux866, dc)
new_gt(xux1977, xux1972, app(app(ty_Either, ca), cb)) → error([])
new_splitGT8(EmptyFM, xux4000, h) → new_emptyFM0(h)
new_primMulNat(xux500) → new_primPlusNat0(new_primPlusNat0(new_primMulNat0(xux500), Succ(xux500)), Succ(xux500))
new_mkBalBranch6MkBalBranch56(xux5260, xux5261, xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, xux5264, True, ba, bb) → new_mkBranch1(xux5260, xux5261, new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5263, ba, bb), xux5264, ba, bb)
new_splitLT9(EmptyFM, h) → new_emptyFM0(h)
new_lt0(xux528, xux5220, ty_Integer) → error([])
new_gt0(Neg(Zero), Neg(Zero)) → new_esEs9
new_esEs5 → False
new_gt0(Pos(Zero), Pos(Zero)) → new_esEs9
new_lt0(xux528, xux5220, app(ty_Ratio, ga)) → error([])
new_addToFM_C(EmptyFM, xux1977, xux1978, bc, bd) → Branch(xux1977, xux1978, Pos(Succ(Zero)), new_emptyFM(bc, bd), new_emptyFM(bc, bd))
new_gt(xux1977, xux1972, ty_Float) → error([])
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Neg(Succ(xux195500)), ba, bb) → new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195500, Zero, ba, bb)
new_ps(Neg(xux19360), Neg(xux19350)) → Neg(new_primPlusNat0(xux19360, xux19350))
new_splitLT30(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Zero), h) → xux33
new_splitGT23(xux353, xux354, xux355, xux356, xux357, xux358, Zero, Succ(xux3600), da) → new_splitGT24(xux353, xux354, xux355, xux356, xux357, xux358, da)
new_splitGT6(Branch(xux330, xux331, xux332, xux333, xux334), xux4000, h) → new_splitGT30(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), h)
new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, Branch(xux52630, xux52631, xux52632, xux52633, xux52634), ba, bb) → new_mkVBalBranch30(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux52630, xux52631, xux52632, xux52633, xux52634, ba, bb)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, Branch(xux195840, xux195841, xux195842, xux195843, xux195844), False, ba, bb) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))), xux195840, xux195841, new_mkBranch0(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))), xux19580, xux19581, xux19583, xux195843, ba, bb), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))), xux5260, xux5261, xux195844, xux5264, ba, bb)
new_gt(xux1977, xux1972, app(app(app(ty_@3, cc), cd), ce)) → error([])
new_addToFM_C4(EmptyFM, xux40, xux41, h) → Branch(xux40, xux41, Pos(Succ(Zero)), new_emptyFM0(h), new_emptyFM0(h))
new_esEs10(Neg(Succ(xux52800)), Neg(xux5190)) → new_esEs2(xux5190, Succ(xux52800))
new_mkBalBranch6MkBalBranch51(xux1972, xux1973, xux1975, xux1977, xux1978, xux1976, True, bc, bd) → new_mkBranch1(xux1972, xux1973, new_addToFM_C(xux1975, xux1977, xux1978, bc, bd), xux1976, bc, bd)
new_gt(xux1977, xux1972, ty_Char) → error([])
new_mkBranchUnbox(xux5264, xux5260, xux1960, xux1961, ba, bb) → xux1961
new_gt(xux1977, xux1972, ty_Ordering) → error([])
new_gt(xux1977, xux1972, ty_@0) → error([])
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux1956000), Succ(xux1955000), ba, bb) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux1956000, xux1955000, ba, bb)
new_mkVBalBranch4(xux40, xux41, EmptyFM, xux5, h) → new_addToFM0(xux5, xux40, xux41, h)
new_splitGT30(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Zero), h) → xux34
new_gt0(Neg(Zero), Neg(Succ(xux197200))) → new_esEs6(xux197200, Zero)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Neg(Zero), ba, bb) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_splitGT7(Branch(xux340, xux341, xux342, xux343, xux344), h) → new_splitGT30(xux340, xux341, xux342, xux343, xux344, Pos(Zero), h)
new_lt(xux528, xux519) → new_esEs10(xux528, xux519)
new_splitGT30(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), h) → new_mkVBalBranch4(Neg(Zero), xux31, new_splitGT6(xux33, xux4000, h), xux34, h)
new_splitGT23(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux3590), Zero, da) → new_splitGT6(xux357, xux358, da)
new_mkVBalBranch3MkVBalBranch20(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, False, ba, bb) → new_mkVBalBranch3MkVBalBranch10(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, new_lt(new_sr0(new_mkVBalBranch3Size_r(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb)), new_mkVBalBranch3Size_l(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb)), ba, bb)
new_esEs10(Pos(Succ(xux52800)), Pos(xux5190)) → new_esEs2(Succ(xux52800), xux5190)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, xux19584, True, ba, bb) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))), xux19580, xux19581, xux19583, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))), xux5260, xux5261, xux19584, xux5264, ba, bb)
new_sr0(xux1919) → new_primMulInt(xux1919)
new_gt0(Pos(Zero), Pos(Succ(xux197200))) → new_esEs11(Zero, xux197200)
new_primMinusNat0(Zero, Succ(xux12430)) → Neg(Succ(xux12430))
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Zero, Zero, ba, bb) → new_mkBalBranch6MkBalBranch44(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_mkVBalBranch4(xux40, xux41, Branch(xux60, xux61, xux62, xux63, xux64), EmptyFM, h) → new_addToFM0(Branch(xux60, xux61, xux62, xux63, xux64), xux40, xux41, h)
new_lt0(xux528, xux5220, app(app(ty_@2, fa), fb)) → error([])
new_splitLT6(EmptyFM, xux4000, h) → new_emptyFM0(h)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Succ(xux195600)), Pos(xux19550), ba, bb) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_splitGT30(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), h) → new_splitGT9(xux34, h)
new_splitGT11(xux834, xux835, xux836, xux837, xux838, xux839, Succ(xux8400), Zero, de) → new_splitGT12(xux834, xux835, xux836, xux837, xux838, xux839, de)
new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb) → new_mkBalBranch6MkBalBranch47(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_splitGT30(Neg(xux300), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), h) → new_splitGT8(xux34, xux4000, h)
new_splitLT7(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, h) → new_splitLT30(xux340, xux341, xux342, xux343, xux344, Pos(Succ(xux4000)), h)
new_splitGT30(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), h) → new_splitGT7(xux34, h)
new_splitGT30(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), h) → new_mkVBalBranch4(Pos(Succ(xux3000)), xux31, new_splitGT9(xux33, h), xux34, h)
new_esEs8 → True
new_splitLT30(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Zero), h) → new_splitLT9(xux33, h)
new_gt0(Neg(Zero), Pos(Succ(xux197200))) → new_esEs5
new_splitGT11(xux834, xux835, xux836, xux837, xux838, xux839, Succ(xux8400), Succ(xux8410), de) → new_splitGT11(xux834, xux835, xux836, xux837, xux838, xux839, xux8400, xux8410, de)
new_mkVBalBranch3MkVBalBranch10(xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, xux528, xux529, False, ba, bb) → new_mkBranch2(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))), xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb)
new_splitLT14(xux852, xux853, xux854, xux855, xux856, xux857, dd) → xux855
new_splitGT11(xux834, xux835, xux836, xux837, xux838, xux839, Zero, Succ(xux8410), de) → new_mkVBalBranch4(Pos(Succ(xux834)), xux835, new_splitGT8(xux837, xux839, de), xux838, de)
new_ps(Pos(xux19360), Neg(xux19350)) → new_primMinusNat0(xux19360, xux19350)
new_ps(Neg(xux19360), Pos(xux19350)) → new_primMinusNat0(xux19350, xux19360)
new_splitLT26(xux362, xux363, xux364, xux365, xux366, xux367, Succ(xux3680), Zero, db) → new_splitLT24(xux362, xux363, xux364, xux365, xux366, xux367, db)
new_mkBalBranch6Size_r(xux5260, xux5261, xux1875, xux5264, ba, bb) → new_sizeFM(xux5264, ba, bb)
new_splitLT25(xux371, xux372, xux373, xux374, xux375, xux376, Zero, Zero, cg) → new_splitLT23(xux371, xux372, xux373, xux374, xux375, xux376, cg)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Pos(Succ(xux195600)), Neg(xux19550), ba, bb) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_splitGT13(xux843, xux844, xux845, xux846, xux847, xux848, Succ(xux8490), Zero, gb) → new_splitGT14(xux843, xux844, xux845, xux846, xux847, xux848, gb)
new_gt0(Pos(Succ(xux197700)), Pos(xux19720)) → new_esEs6(xux197700, xux19720)
new_esEs10(Neg(Succ(xux52800)), Pos(xux5190)) → new_esEs4
new_sr(Neg(xux20120)) → Neg(new_primMulNat2(xux20120))
new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, False, ee, ef) → new_mkBalBranch6MkBalBranch40(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, ee, ef), xux1992, new_mkBalBranch6Size_r(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, ee, ef), ee, ef), new_sr0(new_mkBalBranch6Size_l(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, ee, ef), ee, ef)), ee, ef)
new_mkBranch(xux2028, xux2029, xux2030, xux2031, xux2032, xux2033, xux2034, xux2035, xux2036, ec, ed) → new_mkBranchResult(xux2029, xux2030, new_mkBranch0(xux2032, xux2033, xux2034, xux2035, xux2036, ec, ed), xux2031, ec, ed)
new_primMulInt(xux1859) → new_primMulInt0(xux1859)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Zero), Pos(Succ(xux195500)), ba, bb) → new_mkBalBranch6MkBalBranch45(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_splitGT14(xux843, xux844, xux845, xux846, xux847, xux848, gb) → xux847
new_esEs10(Pos(Zero), Neg(Succ(xux51900))) → new_esEs3
new_gt0(Pos(Zero), Neg(Succ(xux197200))) → new_esEs8
new_splitGT13(xux843, xux844, xux845, xux846, xux847, xux848, Zero, Zero, gb) → new_splitGT14(xux843, xux844, xux845, xux846, xux847, xux848, gb)
new_splitGT26(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux3500), Succ(xux3510), eb) → new_splitGT26(xux344, xux345, xux346, xux347, xux348, xux349, xux3500, xux3510, eb)
new_lt0(xux528, xux5220, ty_@0) → error([])
new_gt(xux1977, xux1972, app(ty_Maybe, be)) → error([])
new_esEs10(Neg(Zero), Neg(Zero)) → new_esEs1
new_primPlusNat0(Succ(xux1020000), Succ(xux542000)) → Succ(Succ(new_primPlusNat0(xux1020000, xux542000)))
new_esEs7(Zero, Zero) → new_esEs9
new_esEs7(Zero, Succ(xux1972000)) → new_esEs5
new_lt0(xux528, xux5220, ty_Int) → new_lt(xux528, xux5220)
new_splitGT23(xux353, xux354, xux355, xux356, xux357, xux358, Succ(xux3590), Succ(xux3600), da) → new_splitGT23(xux353, xux354, xux355, xux356, xux357, xux358, xux3590, xux3600, da)
new_splitLT30(Neg(xux300), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), h) → new_mkVBalBranch4(Neg(xux300), xux31, xux33, new_splitLT7(xux34, xux4000, h), h)
new_splitGT30(Neg(Zero), xux31, xux32, xux33, xux34, Neg(Zero), h) → xux34
new_gt(xux1977, xux1972, ty_Double) → error([])
new_esEs6(xux197700, Zero) → new_esEs8
new_mkVBalBranch(xux528, xux529, xux5220, xux5221, xux5222, xux5223, xux5224, EmptyFM, ba, bb) → new_addToFM(xux5220, xux5221, xux5222, xux5223, xux5224, xux528, xux529, ba, bb)
new_splitGT9(EmptyFM, h) → new_emptyFM0(h)
new_splitLT30(Neg(Succ(xux3000)), xux31, xux32, xux33, xux34, Neg(Succ(xux4000)), h) → new_splitLT25(xux3000, xux31, xux32, xux33, xux34, xux4000, xux3000, xux4000, h)
new_splitLT30(Pos(Succ(xux3000)), xux31, xux32, xux33, xux34, Pos(Zero), h) → new_splitLT8(xux33, h)
new_primMinusNat0(Succ(xux129700), Zero) → Pos(Succ(xux129700))
new_primMulNat3(Succ(xux184000)) → new_primPlusNat0(new_primMulNat1(xux184000), Succ(xux184000))
new_sizeFM(EmptyFM, df, dg) → Pos(Zero)
new_splitGT26(xux344, xux345, xux346, xux347, xux348, xux349, Succ(xux3500), Zero, eb) → new_splitGT8(xux348, xux349, eb)
new_esEs10(Pos(Zero), Pos(Succ(xux51900))) → new_esEs2(Zero, Succ(xux51900))
new_esEs2(Zero, Zero) → new_esEs1
new_mkBalBranch6MkBalBranch41(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, Succ(xux195500), ba, bb) → new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, xux195600, xux195500, ba, bb)
new_splitGT11(xux834, xux835, xux836, xux837, xux838, xux839, Zero, Zero, de) → new_splitGT12(xux834, xux835, xux836, xux837, xux838, xux839, de)
new_mkBalBranch6MkBalBranch01(xux5260, xux5261, xux1959, xux52640, xux52641, xux52642, EmptyFM, xux52644, xux1958, False, ba, bb) → error([])
new_splitLT30(Pos(Zero), xux31, xux32, xux33, xux34, Pos(Succ(xux4000)), h) → new_mkVBalBranch4(Pos(Zero), xux31, xux33, new_splitLT7(xux34, xux4000, h), h)
new_esEs11(Succ(xux197200), xux197700) → new_esEs7(xux197200, xux197700)
new_lt0(xux528, xux5220, app(ty_Maybe, eg)) → error([])
new_lt0(xux528, xux5220, ty_Double) → error([])
new_esEs3 → False
new_splitGT6(EmptyFM, xux4000, h) → new_emptyFM0(h)
new_addToFM_C10(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, False, ee, ef) → Branch(xux1994, xux1995, xux1991, xux1992, xux1993)
new_addToFM_C10(xux1989, xux1990, xux1991, xux1992, xux1993, xux1994, xux1995, True, ee, ef) → new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, new_lt(new_ps(new_mkBalBranch6Size_l(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, ee, ef), ee, ef), new_mkBalBranch6Size_r(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, ee, ef), ee, ef)), Pos(Succ(Succ(Zero)))), ee, ef)
new_primMulNat2(Zero) → Zero
new_mkBalBranch6MkBalBranch46(xux5260, xux5261, xux1959, xux5264, xux1958, Succ(xux1956000), Zero, ba, bb) → new_mkBalBranch6MkBalBranch42(xux5260, xux5261, xux1959, xux5264, xux1958, ba, bb)
new_mkBalBranch6MkBalBranch40(xux5260, xux5261, xux1959, xux5264, xux1958, Neg(Succ(xux195600)), Neg(xux19550), ba, bb) → new_mkBalBranch6MkBalBranch43(xux5260, xux5261, xux1959, xux5264, xux1958, xux19550, xux195600, ba, bb)
new_mkBalBranch6MkBalBranch11(xux5260, xux5261, xux1959, xux5264, xux19580, xux19581, xux19582, xux19583, EmptyFM, False, ba, bb) → error([])
new_emptyFM0(h) → EmptyFM
new_esEs2(Succ(xux5200000000), Succ(xux18190)) → new_esEs2(xux5200000000, xux18190)
new_gt0(Neg(Succ(xux197700)), Neg(xux19720)) → new_esEs11(xux19720, xux197700)
new_lt0(xux528, xux5220, ty_Ordering) → error([])
new_mkBalBranch6MkBalBranch52(xux1989, xux1990, xux1992, xux1993, xux1994, xux1995, True, ee, ef) → new_mkBranch1(xux1989, xux1990, xux1992, new_addToFM_C(xux1993, xux1994, xux1995, ee, ef), ee, ef)
new_esEs10(Neg(Zero), Neg(Succ(xux51900))) → new_esEs2(Succ(xux51900), Zero)
new_addToFM0(xux5, xux40, xux41, h) → new_addToFM_C4(xux5, xux40, xux41, h)
new_splitGT7(EmptyFM, h) → new_emptyFM0(h)
new_splitLT11(xux861, xux862, xux863, xux864, xux865, xux866, Succ(xux8670), Zero, dc) → new_mkVBalBranch4(Neg(Succ(xux861)), xux862, xux864, new_splitLT6(xux865, xux866, dc), dc)
new_splitGT9(Branch(xux340, xux341, xux342, xux343, xux344), h) → new_splitGT30(xux340, xux341, xux342, xux343, xux344, Neg(Zero), h)
new_splitLT25(xux371, xux372, xux373, xux374, xux375, xux376, Succ(xux3770), Zero, cg) → new_splitLT23(xux371, xux372, xux373, xux374, xux375, xux376, cg)
new_mkBalBranch6MkBalBranch55(xux5220, xux5221, xux5223, xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, False, ba, bb) → new_mkBalBranch6MkBalBranch40(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb), xux5223, new_mkBalBranch6Size_r(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb), ba, bb), new_sr0(new_mkBalBranch6Size_l(xux5220, xux5221, xux5223, new_mkVBalBranch1(xux528, xux529, xux5224, xux5260, xux5261, xux5262, xux5263, xux5264, ba, bb), ba, bb)), ba, bb)
new_primPlusNat0(Succ(xux1020000), Zero) → Succ(xux1020000)
new_primPlusNat0(Zero, Succ(xux542000)) → Succ(xux542000)
new_gt0(Pos(Zero), Neg(Zero)) → new_esEs9
new_gt0(Neg(Zero), Pos(Zero)) → new_esEs9
new_splitLT12(xux852, xux853, xux854, xux855, xux856, xux857, Succ(xux8580), Succ(xux8590), dd) → new_splitLT12(xux852, xux853, xux854, xux855, xux856, xux857, xux8580, xux8590, dd)
new_primMinusNat0(Succ(xux129700), Succ(xux12430)) → new_primMinusNat0(xux129700, xux12430)
new_splitLT30(Pos(Zero), xux31, xux32, xux33, xux34, Neg(Zero), h) → xux33
new_splitLT30(Neg(Zero), xux31, xux32, xux33, xux34, Pos(Zero), h) → xux33
new_splitLT6(Branch(xux330, xux331, xux332, xux333, xux334), xux4000, h) → new_splitLT30(xux330, xux331, xux332, xux333, xux334, Neg(Succ(xux4000)), h)
new_mkVBalBranch1(x0, x1, Branch(x2, x3, x4, x5, x6), x7, x8, x9, x10, x11, x12, x13)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Succ(x5)), Neg(x6), x7, x8)
new_mkBranchResult(x0, x1, x2, x3, x4, x5)
new_mkBalBranch6MkBalBranch55(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, True, x11, x12)
new_mkBalBranch6MkBalBranch51(x0, x1, x2, x3, x4, x5, True, x6, x7)
new_splitLT6(EmptyFM, x0, x1)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Pos(Zero), x5, x6)
new_splitLT13(x0, x1, x2, x3, x4, x5, x6)
new_splitGT30(Neg(Zero), x0, x1, x2, x3, Neg(Zero), x4)
new_splitGT13(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_mkVBalBranch4(x0, x1, EmptyFM, x2, x3)
new_mkBalBranch6MkBalBranch43(x0, x1, x2, x3, x4, Succ(x5), x6, x7, x8)
new_mkBalBranch6MkBalBranch56(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, True, x11, x12)
new_gt0(Pos(Succ(x0)), Pos(x1))
new_emptyFM0(x0)
new_splitLT8(EmptyFM, x0)
new_splitLT25(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_primMinusNat0(Zero, Zero)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, EmptyFM, False, x8, x9)
new_esEs5
new_lt0(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, Branch(x4, x5, x6, x7, x8), True, x9, x10)
new_splitGT11(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_splitLT9(Branch(x0, x1, x2, x3, x4), x5)
new_splitGT26(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_splitLT7(EmptyFM, x0, x1)
new_splitGT23(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_esEs10(Neg(Zero), Neg(Succ(x0)))
new_splitLT30(Neg(Zero), x0, x1, x2, x3, Neg(Succ(x4)), x5)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_splitLT30(Neg(Succ(x0)), x1, x2, x3, x4, Neg(Succ(x5)), x6)
new_splitLT30(Neg(x0), x1, x2, x3, x4, Pos(Succ(x5)), x6)
new_splitLT30(Pos(x0), x1, x2, x3, x4, Neg(Succ(x5)), x6)
new_esEs7(Succ(x0), Succ(x1))
new_splitLT11(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_splitGT30(Pos(Zero), x0, x1, x2, x3, Pos(Zero), x4)
new_primMulNat(x0)
new_gt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_splitLT30(Pos(Zero), x0, x1, x2, x3, Pos(Zero), x4)
new_lt0(x0, x1, app(app(ty_@2, x2), x3))
new_lt0(x0, x1, app(app(ty_Either, x2), x3))
new_splitLT30(Neg(Succ(x0)), x1, x2, x3, x4, Neg(Zero), x5)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Neg(Zero), x5, x6)
new_primMulInt0(Neg(x0))
new_primMulNat2(Succ(x0))
new_mkBalBranch6Size_l(x0, x1, x2, x3, x4, x5)
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_mkBalBranch6MkBalBranch44(x0, x1, x2, x3, x4, x5, x6)
new_mkVBalBranch4(x0, x1, Branch(x2, x3, x4, x5, x6), Branch(x7, x8, x9, x10, x11), x12)
new_splitGT8(Branch(x0, x1, x2, x3, x4), x5, x6)
new_splitLT12(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_mkBalBranch6MkBalBranch41(x0, x1, x2, x3, x4, x5, Succ(x6), x7, x8)
new_mkBranch0(x0, x1, x2, x3, x4, x5, x6)
new_esEs8
new_esEs6(x0, Succ(x1))
new_splitGT8(EmptyFM, x0, x1)
new_splitGT26(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_gt(x0, x1, app(app(ty_Either, x2), x3))
new_sizeFM(EmptyFM, x0, x1)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Succ(x5)), Pos(x6), x7, x8)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Succ(x5)), Neg(x6), x7, x8)
new_splitLT30(Pos(Zero), x0, x1, x2, x3, Neg(Zero), x4)
new_splitLT30(Neg(Zero), x0, x1, x2, x3, Pos(Zero), x4)
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs10(Neg(Zero), Pos(Zero))
new_esEs10(Pos(Zero), Neg(Zero))
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, EmptyFM, x6, x7, False, x8, x9)
new_esEs3
new_splitGT11(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_splitGT6(Branch(x0, x1, x2, x3, x4), x5, x6)
new_splitGT23(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_mkBalBranch6MkBalBranch42(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, x9, x10)
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_gt0(Pos(Zero), Neg(Zero))
new_gt0(Neg(Zero), Pos(Zero))
new_primMulInt(x0)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Neg(Succ(x5)), x6, x7)
new_primPlusNat0(Succ(x0), Zero)
new_esEs7(Succ(x0), Zero)
new_addToFM(x0, x1, x2, x3, x4, x5, x6, x7, x8)
new_splitLT26(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_addToFM0(x0, x1, x2, x3)
new_splitGT11(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_mkBalBranch6MkBalBranch47(x0, x1, x2, x3, x4, x5, x6)
new_splitGT30(Pos(Succ(x0)), x1, x2, x3, x4, Pos(Succ(x5)), x6)
new_ps(Pos(x0), Pos(x1))
new_lt0(x0, x1, ty_Double)
new_splitLT30(Pos(Succ(x0)), x1, x2, x3, x4, Pos(Zero), x5)
new_esEs11(Zero, x0)
new_splitLT12(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_esEs10(Neg(Zero), Neg(Zero))
new_esEs6(x0, Zero)
new_esEs2(Zero, Succ(x0))
new_splitLT6(Branch(x0, x1, x2, x3, x4), x5, x6)
new_primMinusNat0(Succ(x0), Zero)
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, EmptyFM, True, x4, x5)
new_esEs10(Pos(Zero), Neg(Succ(x0)))
new_esEs10(Neg(Zero), Pos(Succ(x0)))
new_splitLT11(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Zero, Zero, x5, x6)
new_addToFM_C30(x0, x1, x2, x3, x4, x5, x6, x7, x8)
new_sr(Pos(x0))
new_splitGT30(Pos(x0), x1, x2, x3, x4, Neg(Succ(x5)), x6)
new_splitGT30(Neg(x0), x1, x2, x3, x4, Pos(Succ(x5)), x6)
new_esEs2(Succ(x0), Succ(x1))
new_primMulNat1(x0)
new_esEs1
new_splitGT13(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_splitLT30(Neg(Succ(x0)), x1, x2, x3, x4, Pos(Zero), x5)
new_splitLT30(Pos(Succ(x0)), x1, x2, x3, x4, Neg(Zero), x5)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Neg(Zero), x5, x6)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Pos(Zero), x5, x6)
new_primMinusNat0(Succ(x0), Succ(x1))
new_splitLT30(Neg(Zero), x0, x1, x2, x3, Neg(Zero), x4)
new_splitGT9(Branch(x0, x1, x2, x3, x4), x5)
new_mkBalBranch6MkBalBranch42(x0, x1, x2, EmptyFM, x3, x4, x5)
new_splitLT11(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_mkVBalBranch30(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
new_emptyFM(x0, x1)
new_primMulNat3(Zero)
new_mkBranchUnbox(x0, x1, x2, x3, x4, x5)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, Branch(x6, x7, x8, x9, x10), x11, x12, False, x13, x14)
new_splitGT24(x0, x1, x2, x3, x4, x5, x6)
new_splitGT30(Pos(Zero), x0, x1, x2, x3, Pos(Succ(x4)), x5)
new_splitLT26(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_lt0(x0, x1, app(ty_Ratio, x2))
new_gt0(Neg(Succ(x0)), Neg(x1))
new_mkBranch(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, Branch(x8, x9, x10, x11, x12), False, x13, x14)
new_esEs2(Zero, Zero)
new_gt(x0, x1, ty_Float)
new_splitGT30(Neg(Succ(x0)), x1, x2, x3, x4, Pos(Zero), x5)
new_splitGT30(Pos(Succ(x0)), x1, x2, x3, x4, Neg(Zero), x5)
new_ps(Neg(x0), Neg(x1))
new_splitLT30(Pos(Succ(x0)), x1, x2, x3, x4, Pos(Succ(x5)), x6)
new_gt(x0, x1, ty_@0)
new_gt0(Pos(Zero), Pos(Succ(x0)))
new_gt(x0, x1, app(app(ty_@2, x2), x3))
new_splitLT11(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_lt0(x0, x1, ty_Float)
new_gt0(Pos(Zero), Neg(Succ(x0)))
new_gt0(Neg(Zero), Pos(Succ(x0)))
new_gt(x0, x1, ty_Char)
new_mkVBalBranch1(x0, x1, EmptyFM, x2, x3, x4, x5, x6, x7, x8)
new_gt(x0, x1, ty_Ordering)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Zero, Succ(x5), x6, x7)
new_mkVBalBranch3Size_r(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_splitGT26(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_mkVBalBranch3MkVBalBranch20(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, True, x12, x13)
new_mkVBalBranch(x0, x1, x2, x3, x4, x5, x6, EmptyFM, x7, x8)
new_mkVBalBranch4(x0, x1, Branch(x2, x3, x4, x5, x6), EmptyFM, x7)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Succ(x5), Zero, x6, x7)
new_splitGT7(EmptyFM, x0)
new_primMulNat3(Succ(x0))
new_esEs7(Zero, Zero)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Pos(Succ(x5)), x6, x7)
new_splitGT9(EmptyFM, x0)
new_splitLT12(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_mkBalBranch6MkBalBranch52(x0, x1, x2, x3, x4, x5, False, x6, x7)
new_splitLT30(Pos(Zero), x0, x1, x2, x3, Pos(Succ(x4)), x5)
new_lt0(x0, x1, ty_@0)
new_splitLT12(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_splitGT14(x0, x1, x2, x3, x4, x5, x6)
new_gt(x0, x1, ty_Bool)
new_ps(Neg(x0), Pos(x1))
new_ps(Pos(x0), Neg(x1))
new_mkBalBranch6Size_r(x0, x1, x2, x3, x4, x5)
new_splitGT7(Branch(x0, x1, x2, x3, x4), x5)
new_splitGT30(Neg(Succ(x0)), x1, x2, x3, x4, Neg(Zero), x5)
new_splitLT25(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_gt(x0, x1, app(ty_Ratio, x2))
new_mkVBalBranch3MkVBalBranch20(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_splitLT7(Branch(x0, x1, x2, x3, x4), x5, x6)
new_addToFM_C4(EmptyFM, x0, x1, x2)
new_gt(x0, x1, ty_Integer)
new_mkBalBranch6MkBalBranch45(x0, x1, x2, x3, x4, x5, x6)
new_mkVBalBranch3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_addToFM_C(Branch(x0, x1, x2, x3, x4), x5, x6, x7, x8)
new_lt0(x0, x1, ty_Ordering)
new_gt(x0, x1, ty_Double)
new_lt0(x0, x1, ty_Char)
new_splitLT9(EmptyFM, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_lt0(x0, x1, ty_Bool)
new_gt(x0, x1, app(ty_[], x2))
new_mkVBalBranch3MkVBalBranch10(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, True, x12, x13)
new_splitLT26(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_esEs9
new_splitGT30(Neg(Succ(x0)), x1, x2, x3, x4, Neg(Succ(x5)), x6)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Succ(x0))
new_splitLT25(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_splitGT23(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_addToFM_C4(Branch(x0, x1, x2, x3, x4), x5, x6, x7)
new_primMulNat0(x0)
new_esEs10(Pos(Succ(x0)), Neg(x1))
new_esEs10(Neg(Succ(x0)), Pos(x1))
new_gt0(Pos(Succ(x0)), Neg(x1))
new_gt0(Neg(Succ(x0)), Pos(x1))
new_splitGT30(Neg(Zero), x0, x1, x2, x3, Pos(Zero), x4)
new_splitGT30(Pos(Zero), x0, x1, x2, x3, Neg(Zero), x4)
new_mkBalBranch6MkBalBranch52(x0, x1, x2, x3, x4, x5, True, x6, x7)
new_esEs7(Zero, Succ(x0))
new_splitLT26(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_sr0(x0)
new_splitGT23(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_splitLT25(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_esEs4
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_esEs10(Neg(Succ(x0)), Neg(x1))
new_lt(x0, x1)
new_mkBalBranch6MkBalBranch51(x0, x1, x2, x3, x4, x5, False, x6, x7)
new_splitGT12(x0, x1, x2, x3, x4, x5, x6)
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Neg(Zero), Pos(Succ(x5)), x6, x7)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Zero), Neg(Succ(x5)), x6, x7)
new_splitGT6(EmptyFM, x0, x1)
new_esEs10(Pos(Zero), Pos(Succ(x0)))
new_splitLT8(Branch(x0, x1, x2, x3, x4), x5)
new_splitGT11(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_splitGT26(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_mkVBalBranch(x0, x1, x2, x3, x4, x5, x6, Branch(x7, x8, x9, x10, x11), x12, x13)
new_primPlusNat0(Zero, Zero)
new_mkVBalBranch3MkVBalBranch10(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_primMulInt0(Pos(x0))
new_splitLT24(x0, x1, x2, x3, x4, x5, x6)
new_splitLT23(x0, x1, x2, x3, x4, x5, x6)
new_gt0(Neg(Zero), Neg(Zero))
new_mkBranch2(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)
new_esEs11(Succ(x0), x1)
new_esEs10(Pos(Succ(x0)), Pos(x1))
new_primMulNat2(Zero)
new_addToFM_C(EmptyFM, x0, x1, x2, x3)
new_esEs2(Succ(x0), Zero)
new_mkBalBranch6MkBalBranch43(x0, x1, x2, x3, x4, Zero, x5, x6, x7)
new_splitGT13(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_lt0(x0, x1, ty_Int)
new_gt0(Neg(Zero), Neg(Succ(x0)))
new_lt0(x0, x1, app(ty_Maybe, x2))
new_gt0(Pos(Zero), Pos(Zero))
new_mkBranch1(x0, x1, x2, x3, x4, x5)
new_splitGT30(Neg(Zero), x0, x1, x2, x3, Neg(Succ(x4)), x5)
new_splitLT14(x0, x1, x2, x3, x4, x5, x6)
new_mkBalBranch6MkBalBranch41(x0, x1, x2, x3, x4, x5, Zero, x6, x7)
new_esEs10(Pos(Zero), Pos(Zero))
new_sr(Neg(x0))
new_splitGT30(Pos(Succ(x0)), x1, x2, x3, x4, Pos(Zero), x5)
new_splitGT13(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_mkBalBranch6MkBalBranch40(x0, x1, x2, x3, x4, Pos(Succ(x5)), Pos(x6), x7, x8)
new_gt(x0, x1, ty_Int)
new_lt0(x0, x1, ty_Integer)
new_gt(x0, x1, app(ty_Maybe, x2))
new_lt0(x0, x1, app(ty_[], x2))
new_mkBalBranch6MkBalBranch55(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
new_mkBalBranch6MkBalBranch46(x0, x1, x2, x3, x4, Succ(x5), Succ(x6), x7, x8)
new_splitGT25(x0, x1, x2, x3, x4, x5, x6)
new_mkBalBranch6MkBalBranch56(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
From the DPs we obtained the following set of size-change graphs: